Improve typechecking of let-bindings
[ghc.git] / testsuite / tests / indexed-types / should_fail / T3330a.hs
1 {-# LANGUAGE FlexibleContexts #-}
2 {-# LANGUAGE RankNTypes #-}
3 {-# LANGUAGE TypeFamilies #-}
4
5 -- A very bogus program (multiple errors) but
6 -- sent GHC 6.12 into a loop
7
8 module T3330a where
9
10 newtype Writer w a = Writer { runWriter :: (a, w) }
11 execWriter :: Writer w a -> w
12 execWriter m = snd (runWriter m)
13
14 data AnyF (s :: * -> *) = AnyF
15 class HFunctor (f :: (* -> *) -> * -> *)
16 type family PF (phi :: * -> *) :: (* -> *) -> * -> *
17
18 children :: s ix -> (PF s) r ix -> [AnyF s]
19 children p x = execWriter (hmapM p collect x)
20
21 {-
22 0 from instantiating hmap
23 2 from instantiating collect
24
25 (forall ixx. (phi0 ixx -> r0 ixx -> m0 (r'0 ixx) ~ s ix))
26 phi0 ix0 ~ s2 ix2 -> r2 ix2 -> Writer [AnyF s2] (r2 ix2)
27 f0 r0 ix0 ~ PF s r ix
28 m0 (f0 r'0 ix0) ~ Writer [AnyF s] a0
29
30 Hence ix0 := ix
31 r0 := r
32 f0 := PF s
33 phi0 := (->) s2 ix2
34 m0 := Writer [AnyF s]
35 a0 : = f0 r'0 ix0
36
37 (forall ixx. ((->) (s2 ix2 -> ixx) (r ixx -> Writer [AnyF s] (r'0 ixx)) ~ s ix))
38
39 s2 ix2 ix0 ~ (->) (s2 ix2) (r2 ix2 -> Writer [AnyF s2] (r2 ix2))
40
41 -}
42
43 collect :: HFunctor (PF s) => s ix -> r ix -> Writer [AnyF s] (r ix)
44 collect = error "collect"
45
46 hmapM :: (forall ix. phi ix -> r ix -> m (r' ix))
47 -> phi ix -> f r ix -> m (f r' ix)
48 hmapM _ = error "hmapM"