blob: 62798fad39c1a99697a73926408d5de71fc3ae0e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
|
{-# LANGUAGE TypeFamilies, FunctionalDependencies, FlexibleContexts, GADTs, ScopedTypeVariables #-}
module ExtraTcsUntch where
class C x y | x -> y where
op :: x -> y -> ()
instance C [a] [a]
type family F a :: *
h :: F Int -> ()
h = undefined
data TEx where
TEx :: a -> TEx
f x =
let g1 :: forall b. b -> ()
g1 _ = h [x]
g2 z = case z of TEx y -> (h [[undefined]], op x [y])
in (g1 '3', g2 undefined)
{- This example comes from Note [Extra TcS Untouchables] in TcSimplify. It demonstrates
why when floating equalities out of an implication constraint we must record the free
variables of the equalities as untouchables. With GHC 7.4.1 this program gives a Core
Lint error because of an existential escaping.
assuming x:beta
forall b. F Int ~ [beta] (from g1)
forall a. F Int ~ [[alpha]], C beta [a] (from g2)
-}
{- Assume x:beta
From g1 we get [W] (forall b. F Int ~ [beta])
From g2 we get [W] (forall c. 0 => F Int ~ [[alpha]] /\ C beta [c])
(g2 is not generalised; the forall comes from the TEx pattern)
approximateWC then gives the candidate constraints to quantify
F Int ~ [beta], F Int ~ [[alpha']]
(alpha' is the promoted version of alpha)
Now decide inferred sig for f :: F Int ~ [beta] => beta -> blah
since beta is mentioned in tau-type for f but alpha' is not
Perhaps this is a stupid constraint to generalise over (we don't
generalise over (C Int).
-}
|
