1 {-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, GADTs,

2 UndecidableInstances, RankNTypes, ScopedTypeVariables #-}

16 -- the two k's, even though they have different scopes, should unify in the

17 -- kind-check and then work in the type-check because Prox3 has been generalized

23 -- This probably should be rejected, as it's polymorphic recursion without a CUSK.

24 -- But GHC accepts it because the polymorphic occurrence is at a type variable.

27 -- k and j should unify

32 -- this last example just checks that GADT pattern-matching on kinds still works.

33 -- nothing new here.

38 MkS :: S a

42 y = MkS

45 -- This is questionable. Should we use the RHS to determine dependency? It works

46 -- now, but if it stops working in the future, that's not a deal-breaker.

50 -- This is a challenge. It should be accepted, but only because c's kind is learned

51 -- to be Proxy True, allowing b to be assigned kind `a`. If we don't know c's kind,

52 -- then GHC would need to be convinced that If (c's kind) b d always has kind `a`.

53 -- Naively, we don't know about c's kind early enough.

60 x _ = Proxy

65 where

73 where

77 -- cf. dependent/should_fail/T14066h. Here, y's type does *not* capture any variables,

78 -- so it is generalized, even with MonoLocalBinds.

80 where