
22 Aug
2012
22 Aug
'12
4:50 p.m.
Quoting "Matthew Steele"
1) bar ifn = case ifn of IntFn fn -> foo fn 2) bar ifn = foo (case ifn of IntFn fn -> fn)
I can't help feeling like maybe I am missing some small but important piece from my mental model of how rank-2 types work.
As SPJ suggested, translation to System F with explicit type applications makes the issue clearer: 1) bar = \(ifn :: forall a. IntFn a). case ifn _a of IntFn (fn :: _a -> Int) -> foo (/\a. ???) 2) bar = \(ifn :: forall a. IntFn a). foo (/\a. case ifn a of IntFn (fn :: a -> Int) -> fn) Lauri