Note [Skolemisation]
topSkolemise decomposes and skolemises a type, returning a type
with no top level foralls or (=>).
Examples:
topSkolemise (forall a. Ord a => a -> a)
= ( wp, [a], [d:Ord a], a->a )
where
wp = /\a. \(d:Ord a). <hole> a d
For nested foralls, see Note [Skolemisation en-bloc]
In general,
if topSkolemise ty = (wrap, tvs, evs, rho)
and e :: rho
then wrap e :: ty
and 'wrap' binds {tvs, evs} References 1
- Skolemisation en-bloc GHC.Tc.Utils.Instantiate
Referenced by 2
- GHC.Tc.Utils.Instantiate call site
- GHC.Tc.Utils.Unify call site