testsuite: Add testcase for #13822

Reviewers: austin

Subscribers: rwbarton, thomie

GHC Trac Issues: #13822

Differential Revision: https://phabricator.haskell.org/D3655

testsuite/tests/typecheck/should_compile/T13822.hs

+{-# LANGUAGE GADTs, TypeOperators, PolyKinds, DataKinds, TypeFamilyDependencies, TypeInType, RankNTypes, LambdaCase, EmptyCase #-}
+
+module T13822 where
+
+import Data.Kind
+
+data KIND = STAR | KIND :> KIND
+
+data Ty :: KIND -> Type where
+  TInt   :: Ty STAR
+  TBool  :: Ty STAR
+  TMaybe :: Ty (STAR :> STAR)
+  TApp   :: Ty (a :> b) -> (Ty a -> Ty b)
+
+type family
+  IK (k :: KIND) = (res :: Type) | res -> k where
+  IK STAR   = Type
+  IK (a:>b) = IK a -> IK b
+
+type family
+  I (t :: Ty k) = (res :: IK k) | res -> t where
+  I TInt       = Int
+  I TBool      = Bool
+  I TMaybe     = Maybe
+  I (TApp f a) = (I f) (I a)
+
+data TyRep (k :: KIND) (t :: Ty k) where
+  TyInt   :: TyRep STAR         TInt
+  TyBool  :: TyRep STAR         TBool
+  TyMaybe :: TyRep (STAR:>STAR) TMaybe
+  TyApp   :: TyRep (a:>b) f -> TyRep a x -> TyRep b (TApp f x)
+
+zero :: TyRep STAR a -> I a
+zero = \case
+  TyInt           -> 0
+  TyBool          -> False
+  TyApp TyMaybe _ -> Nothing
+
+
+-- Inferred type:
+--
+-- int :: TyRep STAR TInt -> Int
+int rep = zero rep :: Int
+
+-- bool:: TyRep STAR TBool -> Bool
+bool rep = zero rep :: Bool
+
+-- Previously failed with:
+--
+-- v.hs:43:16: error:
+--     • Couldn't match kind ‘k’ with ‘'STAR’
+--       ‘k’ is a rigid type variable bound by
+--         the inferred type of
+--         maybeInt :: (I 'TInt ~ Int, I 'TMaybe ~ Maybe) =>
+--                     TyRep 'STAR ('TApp 'TMaybe 'TInt) -> Maybe Int
+--         at v.hs:25:3
+--       When matching the kind of ‘'TMaybe’
+--       Expected type: Maybe Int
+--         Actual type: I ('TApp 'TMaybe 'TInt)
+--     • In the expression: zero rep :: Maybe Int
+--       In an equation for ‘maybeInt’: maybeInt rep = zero rep :: Maybe Int
+--     • Relevant bindings include
+--         rep :: TyRep 'STAR ('TApp 'TMaybe 'TInt) (bound at v.hs:43:10)
+--         maybeInt :: TyRep 'STAR ('TApp 'TMaybe 'TInt) -> Maybe Int
+--           (bound at v.hs:43:1)
+-- Failed, modules loaded: none.
+maybeInt rep = zero rep :: Maybe Int

testsuite/tests/typecheck/should_compile/all.T

@@ -563,3 +563,4 @@ test('T13585', [extra_files(['T13585.hs', 'T13585a.hs', 'T13585b.hs'])], run_com
 test('T13651', normal, compile, [''])
 test('T13785', normal, compile, [''])
 test('T13804', normal, compile, [''])
+test('T13822', normal, compile, [''])