[Haskell-cafe] Rigid skolem type variable escaping scope
la at iki.fi
Wed Aug 22 22:50:19 CEST 2012
Quoting "Matthew Steele" <mdsteele at alum.mit.edu>:
> 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)
More information about the Haskell-Cafe