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 in Var, alongside ArgFlag

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 constructor Anon in TyCoRep

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 (in TyCon)

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.

A huge win is that isPredTy vanishes almost completely.

Invariant: in FFunTy af arg res

• If af = InvisArg then arg :: 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.