| Is this intentional?
Yes, it's absolutely intentional.
Consider this Core defn
f :: forall a b. (a ~# b) -> Int
f = /\a b. \(g :: a ~# b). error "urk"
Now is `seq f True` equal to True, or to (error "urk"). Definitely the former.
So we cannot and must not discard coercion lambda.
> > Think of a hypothetical coercion `co :: Int ~ Double`; applying that
> > coercion
> > as in `x |> co` to `x :: Int` would need to `fild` (load the integer in a
> > floating point register) at run-time, so you can't erase it. The fact that
> > we
> > can for newtypes is because `coerce` is
> I'm not sure if there's a case in GHC (yet, because newtype coercions are
> zero-cost), but coercions in general (as introduced for example in Types and
> Programming Languages) can carry computational content and thus can't be
> erased.
But they're already erased! They don't have a runtime
Hi Ömer,
I'm not sure if there's a case in GHC (yet, because newtype coercions are
zero-cost), but coercions in general (as introduced for example in Types
and Programming Languages) can carry computational content and thus can't
be erased.
Think of a hypothetical coercion `co :: Int ~ Double`;
Hi,
I just realized that coercion binders are currently Ids and not TyVars (unlike
other type arguments). This means that we don't drop coercion binders in
CoreToStg. Example:
{-# LANGUAGE ScopedTypeVariables, TypeOperators, PolyKinds, GADTs,
TypeApplications, MagicHash #-}
