summaryrefslogtreecommitdiff
path: root/testsuite/tests/typecheck/should_compile/tc163.hs
blob: 21d8a7294976c3d19029b0beabe7ef7e376bc406 (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
{-# LANGUAGE RankNTypes #-}

-- This one killed GHC 5.05 and earlier
-- The problem was in a newtype with a record selector, with
-- a polymorphic argument type.  MkId generated a bogus selector
-- function

module ShouldCompile where

type M3 a = forall r. (forall b. M3' b -> (b -> M3' a) -> r) -> r

newtype M3' a = M3' { mkM3' :: M3 a }

flop :: forall a b. M3' b -> (b -> M3' a) -> Int
flop = \m' k -> mkM3' m' (\bm k1 -> error "urk")

-- Suppose mkM3' has the straightforward type: 
--     mkM3' :: forall a. M3' a -> M3 a
-- Then (mkM3' m') :: forall r. (forall b. ...) -> r
-- If we simply do a subsumption check of this against
--    alpha -> Int
-- where alpha is the type inferred for (\bm k1 ...) 
-- this won't work.

-- But if we give mkM3' the type 
--     forall a r. M3' a -> (forall b. ...) -> r
-- everthing works fine.  Very very delicate.

---------------- A more complex case -------------
bind :: M3 a -> (a -> M3 b) -> M3 b
bind m k b = b (M3' m) (\a -> M3' (k a))

observe :: M3 a -> a
observe m
      = m (\m' k -> mkM3' m'
                (\bm k1 -> observe (bind (mkM3' bm)
                        (\a -> bind (mkM3' (k1 a)) (\a -> mkM3' (k a)))))
                )