Add an AnonArgFlag to FunTy
In Trac #15952 (closed) Richard and I agreed that it makes sense to add a flag to FunTy
to distinguish (->)
from (=>)
. This ticket tracks progress.
Current state is at: !128 (merged)
See ticket:15952#comment:166657 and ticket:15952#comment:166659.
Main changes:
- Define
AnonArgFlag
inVar
, alongsideArgFlag
data AnonArgFlag
= VisArg -- Used for (->): an ordinary non-dependent arrow
-- The argument is visible in source code
| InvisArg -- Used for (=>): a non-dependent predicate arrow
-- The argument is invisible in source code
-
Type
looks like this
data Type
= ...
| FFunTy -- ^ t1 -> t2 Very common, so an important special case
-- FFunTy for "full function type"; see pattern synonym for FunTy
{ ft_af :: AnonArgFlag -- Is this (->) or (=>)?
, ft_arg :: Type -- Argument type
, ft_res :: Type } -- Resuult type
I'm using a record here to anticipate Linear Haskell, which will add a multiplicity field to
FFunTy
.
- Add a uni-directional pattern synonym for the old
FunTy
pattern FunTy :: Type -> Type -> Type
pattern FunTy arg res <- FFunTy { ft_arg = arg, ft_res = res }
- Add an
AnonArgFlag
to data constructorAnon
inTyCoRep
data TyCoBinder
= Named TyCoVarBinder -- A type-lambda binder
| Anon AnonArgFlag Type -- A term-lambda binder. Type here can be CoercionTy.
-- Visibility is determined by the AnonArgFlag
and to data constructor
AnonTCB
(inTyCon
)
data TyConBndrVis
= NamedTCB ArgFlag
| AnonTCB AnonArgFlag
The latter is needed because the promoted version of a GADT data constructor is a TyCon with some invisible (equality) arguments.
Everything else follows routinely.
isPredTy
vanishes almost completely.
A huge win is that Invariant: in FFunTy af arg res
- If
af
=InvisArg
thenarg :: Constraint
- But not vice versa
When in Core-land, e.g. in the Simplifier, we often call exprType
. What is the type of Lam b e
? Either a ForAllTy
(if b
is a type variable) or a FFunTy
. But what AnonArgFlag
? I propose always VisArg
.
For Core, it really doesn't matter; the AnonArgFlag
only affects the typing of source code. And it is quite painful to call isPredTy
to see if the arg type is Constraint
when the answer doesn't matter. Plus, in Core, Type
and Constraint
coincide, so it seems like a dodgy thing to do anyway.
We could try record the AnonArgFlag
in the Id
; but that means we'd need to call isPredTy
for every Id
we construct.
So for now I propose the above invariant. We make a similar somewhat-arbitrary choice for the ArgFlag
in the TyCoVarBinder
of a ForAllTy
: in exprType (Lam tv b)
we always use Inferred
.
This is also the reason that FunCo
does not have an ArgFlag
; coercions only matter in Core, and are not shown to the user. This does mean that coercionKind co
might not have InvisArg
where you expect; but that's the same problem as with exprType
.