{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE PatternSynonyms           #-}
{-# LANGUAGE RankNTypes                #-}
{-# LANGUAGE PolyKinds                 #-}
{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE TypeOperators             #-}
{-# LANGUAGE ViewPatterns              #-}

module T19622 where

import Data.Kind (Type)

data A
data B

data ElemKind k where
  ElemKindA :: ElemKind A
  ElemKindB :: ElemKind B

class KnownElemKind (xs :: [k]) where
  getKind :: TypedList f xs -> ElemKind k

data TypedList (f :: (k -> Type)) (xs :: [k]) where
  Nil :: TypedList f '[]
  Cons :: f x -> TypedList f xs -> TypedList f (x ': xs)

data Dim (x :: k)

pattern DimA :: forall k (xs :: [k]) . KnownElemKind xs => (k ~ A) => TypedList Dim xs
pattern DimA <- (getKind -> ElemKindA)

{-# COMPLETE DimA #-}
{-# COMPLETE Nil, Cons #-}

f :: forall (xns :: [B]) . TypedList Dim xns -> TypedList Dim xns -> Bool
f Nil Nil = True
f (Cons _ _) (Cons _ _) = True

g :: forall (xns :: [B]) . TypedList Dim xns -> Bool
g Nil = True
g (Cons _ _) = True

h :: forall (xns :: [A]) . TypedList Dim xns -> Bool
h Nil = True
h (Cons _ _) = True

i :: forall (xns :: [A]) . TypedList Dim xns -> TypedList Dim xns -> Bool
i Nil Nil = True
i (Cons _ _) (Cons _ _) = True

j :: forall k (xns :: [k]) . TypedList Dim xns -> TypedList Dim xns -> Bool
j Nil Nil = True
j (Cons _ _) (Cons _ _) = True

l :: forall (xns :: [A]) . KnownElemKind xns => TypedList Dim xns -> Bool
l DimA = True