ExtraTcsUntch.hs 1.46 KB
Newer Older
1 2
{-# LANGUAGE TypeFamilies, FunctionalDependencies, FlexibleContexts, GADTs, ScopedTypeVariables #-}

3
module ExtraTcsUntch where
4 5


6
class C x y | x -> y where
7 8 9 10 11 12 13 14 15
 op :: x -> y -> ()

instance C [a] [a]

type family F a :: *

h :: F Int -> ()
h = undefined

16 17
data TEx where
  TEx :: a -> TEx
18 19


20

21
f x =
22 23
    let g1 :: forall b. b -> ()
        g1 _ = h [x]
24

25
        g2 z = case z of TEx y -> (h [[undefined]], op x [y])
26

27 28 29
    in (g1 '3', g2 undefined)


30
{- This example comes from Note [Extra TcS Untouchables] in TcSimplify. It demonstrates
31 32
   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
33
   Lint error because of an existential escaping.
34 35 36 37 38 39 40 41

    assuming x:beta

    forall b. F Int ~ [beta]                          (from g1)
    forall a. F Int ~ [[alpha]], C beta [a]           (from g2)

-}

42 43


44

45
{- Assume x:beta
46 47 48 49 50 51 52 53 54 55 56 57 58 59 60
   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).
61
-}