content: {-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, GADTs,
               UndecidableInstances, RankNTypes, ScopedTypeVariables #-}
  
  module T14066a where
  
  import Data.Proxy
  import Data.Kind
  import Data.Type.Bool
  
  
  type family Bar x y where
    Bar (x :: a) (y :: b) = Int
    Bar (x :: c) (y :: d) = Bool   -- a,b,c,d should be TyVarTvs and unify appropriately
  
  
    -- the two k's, even though they have different scopes, should unify in the
    -- kind-check and then work in the type-check because Prox3 has been generalized
  
  data Prox3 a where
    MkProx3a :: Prox3 (a :: k1)
    MkProx3b :: Prox3 (a :: k2)
  
    -- This probably should be rejected, as it's polymorphic recursion without a CUSK.
    -- But GHC accepts it because the polymorphic occurrence is at a type variable.
  data T0 a = forall k (b :: k). MkT0 (T0 b) Int
  
    -- k and j should unify
  type family G x a where
    G Int (b :: k) = Int
    G Bool (c :: j) = Bool
  
  -- this last example just checks that GADT pattern-matching on kinds still works.
  -- nothing new here.
  type T :: k -> Type
  data T a where
    MkT :: T (a :: Type -> Type)
  
  data S (a :: Type -> Type) where
    MkS :: S a
  
  f :: forall k (a :: k). Proxy a -> T a -> ()
  f _ MkT = let y :: S a
                y = MkS
            in ()
  
  -- This is questionable. Should we use the RHS to determine dependency? It works
  -- now, but if it stops working in the future, that's not a deal-breaker.
  type P k a = Proxy (a :: k)
  
  
  -- This is a challenge. It should be accepted, but only because c's kind is learned
  -- to be Proxy True, allowing b to be assigned kind `a`. If we don't know c's kind,
  -- then GHC would need to be convinced that If (c's kind) b d always has kind `a`.
  -- Naively, we don't know about c's kind early enough.
  
  data SameKind :: forall k. k -> k -> Type
  
  type IfK :: Proxy (j :: Bool) -> m -> n -> If j m n
  type family IfK e f g where
     IfK (_ :: Proxy True)  f _ = f
     IfK (_ :: Proxy False) _ g = g
  
  x :: forall c. (forall a b (d :: a). SameKind (IfK c b d) d) -> (Proxy (c :: Proxy True))
  x _ = Proxy
  
  
  f2 :: forall b. b -> Proxy Maybe
  f2 x = fstOf3 y :: Proxy Maybe
    where
      y :: (Proxy a, Proxy c, b)
      y = (Proxy, Proxy, x)
  
  fstOf3 (x, _, _) = x
  
  f3 :: forall b. b -> Proxy Maybe
  f3 x = fst y :: Proxy Maybe
    where
      y :: (Proxy a, b)
      y = (Proxy, x)
  
  -- cf. dependent/should_fail/T14066h. Here, y's type does *not* capture any variables,
  -- so it is generalized, even with MonoLocalBinds.
  f4 x = (fst y :: Proxy Int, fst y :: Proxy Maybe)
    where
      y :: (Proxy a, Int)
      y = (Proxy, x)
  