Prioritise class-level equality costraints
[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 nfinite loop
20
21 module T12734a where
22
23 import Prelude
24 import Control.Applicative
25 import Control.Monad.Fix
26 import Control.Monad.Trans.Identity
27 import Control.Monad.Trans.Class
28 import Control.Monad.IO.Class
29
30
31 data A
32 data B
33 data Net
34 data Type
35
36 data Layer4 t l
37 data TermStore
38
39 data Stack lrs (t :: * -> *) where
40 SLayer :: t l -> Stack ls t -> Stack (l ': ls) t
41 SNull :: Stack '[] t
42
43 instance ( Con m (t l)
44 , Con m (Stack ls t)) => Con m (Stack (l ': ls) t)
45 instance Monad m => Con m (Stack '[] t)
46 instance ( expr ~ Expr t lrs
47 , Con m (TStk t lrs)) => Con m (Layer4 expr Type)
48
49
50 newtype Expr t lrs = Expr (TStk t lrs)
51 type TStk t lrs = Stack lrs (Layer4 (Expr t lrs))
52
53
54 class Con m t
55
56
57 -- HERE IS A FUNNY BEHAVIOR: the commented line raises context reduction stack overflow
58 test_gr :: forall m t lrs bind.
59 ( Con m (TStk t lrs)
60 , bind ~ Expr t lrs
61 -- ) => m (Expr t lrs) -- GHC 8 worked if you said this...
62 ) => m bind -- but not this!
63 test_gr = undefined
64
65
66 newtype KT (cls :: *) (t :: k) (m :: * -> *) (a :: *)
67 = KT (IdentityT m a)
68
69 test_ghc_err :: KT A '[Type] IO (Expr Net '[Type])
70
71 test_ghc_err = test_gr @(KT A '[Type] IO) @_ @'[Type] @(Expr Net '[Type])
72
73 {- Works!
74 test_ghc_err = test_gr @(KT A '[Type] IO)
75 @Net
76 @'[Type]
77 @(Expr Net '[Type])
78 -}
79
80 {- Some notes. See comment:10 on Trac #12734
81
82 [W] Con m (TStk t lrs)
83 [W] Inferable A lrs m
84 [W] bind ~ Expr t lrs
85 [W] m bind ~ KT A '[Type] IO (Expr Net '[Type])
86
87 ==> m := KT A '[Type] IO
88 bind := Expr Net '[Type]
89 t := Net
90 lrs := '[Type]
91
92 [W] Con m (TStk t lrs)
93 = Con m (Stack lrs (Layer4 bind))
94 --> inline lrs
95 [W] Con m (Stack '[Type] (Layer4 bind))
96 --> isntance
97 [W] Con m (Stack '[] bind)
98 --> Monad m
99 +
100 [W] Con m (Layer4 bind Type)
101 -->
102 [W] bind ~ Expr t0 lrs0
103 [W] Con m (TStk t0 lrs0)
104 -}