Embrace -XTypeInType, add -XStarIsType
[ghc.git] / testsuite / tests / typecheck / should_compile / T12734a.hs
1 {-# LANGUAGE RankNTypes #-}
2 {-# LANGUAGE FlexibleInstances #-}
3 {-# LANGUAGE FlexibleContexts #-}
4 {-# LANGUAGE MultiParamTypeClasses #-}
5 {-# LANGUAGE FunctionalDependencies #-}
6 {-# LANGUAGE DeriveFunctor #-}
7 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
8 {-# LANGUAGE TypeOperators #-}
9 {-# LANGUAGE DataKinds #-}
10 {-# LANGUAGE NoMonomorphismRestriction #-}
11 {-# LANGUAGE UndecidableInstances #-}
12 {-# LANGUAGE GADTs #-}
13 {-# LANGUAGE PolyKinds #-}
14 {-# LANGUAGE TypeApplications #-}
15
16
17 -- This version is shorter than T12734, and should yield a
18 -- type error message. If things go wrong, you get
19 -- an infinite loop
20
21 module T12734a where
22
23 import Prelude
24 import Data.Kind
25 import Control.Applicative
26 import Control.Monad.Fix
27 import Control.Monad.Trans.Identity
28 import Control.Monad.Trans.Class
29 import Control.Monad.IO.Class
30
31
32 data A
33 data B
34 data Net
35 data Ty
36
37 data Layer4 t l
38 data TermStore
39
40 data Stack lrs (t :: Type -> Type) where
41 SLayer :: t l -> Stack ls t -> Stack (l ': ls) t
42 SNull :: Stack '[] t
43
44 instance ( Con m (t l)
45 , Con m (Stack ls t)) => Con m (Stack (l ': ls) t)
46 instance Monad m => Con m (Stack '[] t)
47 instance ( expr ~ Expr t lrs
48 , Con m (TStk t lrs)) => Con m (Layer4 expr Ty)
49
50
51 newtype Expr t lrs = Expr (TStk t lrs)
52 type TStk t lrs = Stack lrs (Layer4 (Expr t lrs))
53
54
55 class Con m t
56
57
58 -- HERE IS A FUNNY BEHAVIOR: the commented line raises context reduction stack overflow
59 test_gr :: forall m t lrs bind.
60 ( Con m (TStk t lrs)
61 , bind ~ Expr t lrs
62 -- ) => m (Expr t lrs) -- GHC 8 worked if you said this...
63 ) => m bind -- but not this!
64 test_gr = undefined
65
66
67 newtype KT (cls :: Type) (t :: k) (m :: Type -> Type) (a :: Type)
68 = KT (IdentityT m a)
69
70 test_ghc_err :: KT A '[Ty] IO (Expr Net '[Ty])
71
72 test_ghc_err = test_gr @(KT A '[Ty] IO) @_ @'[Ty] @(Expr Net '[Ty])
73
74 {- Works!
75 test_ghc_err = test_gr @(KT A '[Ty] IO)
76 @Net
77 @'[Ty]
78 @(Expr Net '[Ty])
79 -}
80
81 {- Some notes. See comment:10 on Trac #12734
82
83 [W] Con m (TStk t lrs)
84 [W] Inferable A lrs m
85 [W] bind ~ Expr t lrs
86 [W] m bind ~ KT A '[Ty] IO (Expr Net '[Ty])
87
88 ==> m := KT A '[Ty] IO
89 bind := Expr Net '[Ty]
90 t := Net
91 lrs := '[Ty]
92
93 [W] Con m (TStk t lrs)
94 = Con m (Stack lrs (Layer4 bind))
95 --> inline lrs
96 [W] Con m (Stack '[Ty] (Layer4 bind))
97 --> instance
98 [W] Con m (Stack '[] bind)
99 --> Monad m
100 +
101 [W] Con m (Layer4 bind Ty)
102 -->
103 [W] bind ~ Expr t0 lrs0
104 [W] Con m (TStk t0 lrs0)
105 -}