Some primops and wired-in functions are representation-polymorphic, but must
only be instantiated at particular, concrete representations.
There are three cases, all for `hasNoBinding` Ids:
* Wired-in Ids. For example, `seq`
is a wired-in Id, defined in GHC.Types.Id.Make.seqId, with this type:
seq :: forall {r} a (b :: TYPE r). a -> b -> b
It is more like a macro than a regular Id: it has /compulsory/ unfolding, so
we inline it at every call site. At those call sites we should instantiate
`r` with a concrete RuntimeRep, so that the lambda has a concrete representation.
So somehow the type checker has to ensure that `seq` is called with a concrete
instantiation for `r`.
NB: unsafeCoerce# is not quite wired-in (see Note [Wiring in unsafeCoerce#] in GHC.HsToCore),
but it gets a similar treatment.
* PrimOps. Some representation-polymorphic primops must be called at a concrete
type. For example:
catch# :: forall {r} {l} (k :: TYPE r) (w :: TYPE (BoxedRep l)).
(State# RealWorld -> (# State# RealWorld, k #) )
-> (w -> State# RealWorld -> (# State# RealWorld, k #) )
-> State# RealWorld -> (# State# RealWorld, k #)
This primop pushes a "catch frame" on the stack, which must "know"
the return convention of `k`. So `k` must be concrete, so we know
what kind of catch-frame to push. (See #21868 for more details.
So again we want to ensure that `r` is instantiated with a concrete RuntimeRep.
* Unboxed-tuple data constructors. Consider the unboxed pair data constructor:
(#,#) :: forall {r1} {r2} (a :: TYPE r1) (b :: TYPE r2). a -> b -> (# a, b #)
Again, we need concrete `r1` and `r2`. For example, we want to reject
f :: forall r (a :: TYPE r). a -> (# Int, a #)
f = (#,#) 3
As pointed out in #21906; we see here that it is not enough to simply check
the representation of the argument types, as for example "k :: TYPE r" in the
type of catch# occurs in negative position but not directly as the type of
an argument.
NB: we specifically *DO NOT* handle representation-polymorphic unlifted newtypes
with this mechanism. See Note [Eta-expanding rep-poly unlifted newtypes] for an
overview of representation-polymorphism checks for those.
To achieve this goal, for these these three kinds of `hasNoBinding` functions:
* We identify the quantified variable `r` as a "concrete quantifier"
* When instantiating a concrete quantifier, such as `r`, at a call site, we
instantiate with a ConcreteTv meta-tyvar, `r0[conc]`.
See Note [ConcreteTv] in GHC.Tc.Utils.Concrete.
Now the type checker will ensure that `r0` is instantiated with a concrete
RuntimeRep.
Here are the moving parts:
* In the IdDetails of an Id, we record a mapping from type variable name
to concreteness information, in the form of a ConcreteTvOrigin.
See 'idDetailsConcreteTvs'.
The ConcreteTvOrigin is used to determine which error message to show
to the user if the type variable gets instantiated to a non-concrete type;
this is slightly more granular than simply storing a set of type variable names.
* The domain of this NameEnv is the outer forall'd TyVars of that
Id's type. (A bit yukky because it means that alpha-renaming that type
would be invalid. But we never do that.) So `seq` has
Type: forall {r} a (b :: TYPE r). a -> b -> b
IdDetails: RepPolyId [ r :-> ConcreteFRR (FixedRuntimeRepOrigin b (..)) ]
* When instantiating the type of an Id at a call site, at the call to
GHC.Tc.Utils.Instantiate.instantiateSigma in GHC.Tc.Gen.App.tcInstFun,
create ConcreteTv metavariables (instead of TauTvs) based on the
ConcreteTyVars stored in the IdDetails of the Id.
Note that the /only/ place that one of these restricted rep-poly Ids can enter
typechecking is in `tcInferId`, and all the interesting cases then land
in `tcInstFun` where we take care to instantantiate those concrete
type variables correctly.
Design alternative: in some ways, it would be more kosher for the concrete-ness
to be stored in the /type/, thus forall (r[conc] :: RuntimeRep). ty.
But that pollutes Type for a very narrow use-case; so instead we adopt the
more ad-hoc solution described above.
Examples:
ok :: forall (a :: Type) (b :: Type). a -> b -> b
ok = seq
bad :: forall s (b :: TYPE s). Int -> b -> b
bad x = seq x
Here we will instantiate the RuntimeRep skolem variable r from the type
of seq to a concrete metavariable rr[conc].
For 'ok' we will unify rr := LiftedRep, and for 'bad' we will fail to
solve rr[conc] ~# s[sk] and report a representation-polymorphism error to
the user.
type RR :: RuntimeRep
type family RR where { RR = IntRep }
tricky1, tricky2 :: forall (b :: TYPE RR). Int -> b -> b
tricky1 = seq
tricky2 = seq @RR
'tricky1' proceeds as above: we instantiate r |-> rr[conc], get a Wanted
rr[conc] ~# RR, which we solve by rewriting the type family.
For 'tricky2', we again create a fresh ConcreteTv metavariable rr[conc],
and we then proceed as if the user had written "seq @rr", but adding an
additional [W] rr ~ RR to the constraint solving context.
[Wrinkle: VTA]
We must also handle the case when the user has instantiated the type variables
themselves, with a visible type application. We do this in GHC.Tc.Gen.App.tcVTA.
For example:
type F :: Type -> RuntimeRep
type family F a where { F Bool = IntRep }
foo = (# , #) @(F Bool) @FloatRep
We want to accept "foo" even though "F Bool" is not a concrete RuntimeRep.
We proceed as follows (see tcVTA):
- create a fresh concrete metavariable kappa,
- emit [W] F Bool ~ kappa[conc]
- pretend the user wrote (#,#) @kappa.
The solver will then unify kappa := IntRep, after rewriting the type family
application on the LHS of the Wanted.
Note that this is a bit of a corner case: only a few built-ins, such as
unsafeCoerce# and unboxed tuples, have specified (not inferred) RuntimeRep
quantified variables which can be instantiated by the user with a
visible type application.
For example,
coerce :: forall {r :: RuntimeRep} (a :: TYPE r) (b :: TYPE r)
. Coercible a b => a -> b
does not allow the RuntimeRep argument to be specified by a visible type
application.