[commit: ghc] master: testsuite: Add testcase for #13822 (04ca036)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/04ca0360a6b38627c2608ed7468f4d8c46257e3a/ghc

>---------------------------------------------------------------

commit 04ca0360a6b38627c2608ed7468f4d8c46257e3a
Author: Ben Gamari <bgamari.foss at gmail.com>
Date:   Sun Jun 18 16:48:31 2017 -0400

    testsuite: Add testcase for #13822
    
    Reviewers: austin
    
    Subscribers: rwbarton, thomie
    
    GHC Trac Issues: #13822
    
    Differential Revision: https://phabricator.haskell.org/D3655


>---------------------------------------------------------------

04ca0360a6b38627c2608ed7468f4d8c46257e3a
 testsuite/tests/typecheck/should_compile/T13822.hs | 67 ++++++++++++++++++++++
 testsuite/tests/typecheck/should_compile/all.T     |  1 +
 2 files changed, 68 insertions(+)

diff --git a/testsuite/tests/typecheck/should_compile/T13822.hs b/testsuite/tests/typecheck/should_compile/T13822.hs
new file mode 100644
index 0000000..5837cc8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T13822.hs
@@ -0,0 +1,67 @@
+{-# 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
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index a9eb4ff..b267819 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/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, [''])