Testsuite error message changes
[ghc.git] / testsuite / tests / indexed-types / should_fail / GADTwrong1.hs
1 {-# LANGUAGE TypeFamilies, GADTs, RankNTypes, ScopedTypeVariables #-}
2
3 module ShouldFail where
4
5 type family Const a
6 type instance Const a = ()
7
8 data T a where T :: c -> T (Const c)
9
10 coerce :: forall a b . a -> b
11 coerce x = case T x :: T (Const b) of
12 T y -> y
13
14 {-
15 T :: forall a. forall c. (a ~ Const c) => c -> T a
16
17 a ~ gamma -- Instantiate T with a=alpha, c=gamma
18 alpha ~ Const b -- Result of (T x)
19 alpha ~ Const gamma -- Constraint from (T x)
20
21 y::c
22 forall c. (Const b ~ Const c) => c ~ b
23
24 ==>
25 Const b ~ Const a
26
27 ------------
28
29 case e of
30 T y -> y
31
32 e :: T alpha
33
34 Patterns
35 forall c. (alpha ~ Const c) => c ~ b
36 alpha ~ Const b
37
38 -}