Note [Skolemisation]

GHC/Tc/Utils/Instantiate.hs:145 compiler

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

Referenced by 2