f676c294a50a959da989188f69edbc04fb9c76e3
[ghc.git] / testsuite / tests / indexed-types / should_fail / ExtraTcsUntch.hs
1 {-# LANGUAGE TypeFamilies, FunctionalDependencies, FlexibleContexts, GADTs, ScopedTypeVariables #-}
2
3 module ExtraTcsUntch where
4
5
6 class C x y | x -> y where
7 op :: x -> y -> ()
8
9 instance C [a] [a]
10
11 type family F a :: *
12
13 h :: F Int -> ()
14 h = undefined
15
16 data TEx where
17 TEx :: a -> TEx
18
19
20
21 f x =
22 let g1 :: forall b. b -> ()
23 g1 _ = h [x]
24 g2 z = case z of TEx y -> (h [[undefined]], op x [y])
25 in (g1 '3', g2 undefined)
26
27
28 {- This example comes from Note [Extra TcS Untouchables] in TcSimplify. It demonstrates
29 why when floating equalities out of an implication constraint we must record the free
30 variables of the equalities as untouchables. With GHC 7.4.1 this program gives a Core
31 Lint error because of an existential escaping.
32
33 assuming x:beta
34
35 forall b. F Int ~ [beta] (from g1)
36 forall a. F Int ~ [[alpha]], C beta [a] (from g2)
37
38 -}
39
40
41
42
43 {- Assume x:beta
44 From g1 we get (forall b. F Int ~ [beta])
45 From g2 we get (forall c. 0 => F Int ~ [[alpha]] /\ C beta [c])
46
47 Floating we get
48 F Int ~ [beta], F Int ~ [[alpha]], alpha ~ alpha', forall c. C beta [c]
49 = { alpha := alpha' }
50 = beta ~ [alpha'], F Int ~ [[alpha']], forall c. C beta [c]
51 = { beta := [alpha']
52 F Int ~ [[alpha']], forall c. C [alpha'] [c]
53 = F Int ~ [[alpha']], forall c. (C [alpha'] [c], alpha' ~ c)
54 -}