[GHC] #16185: Add an AnonArgFlag to FunTy

[GHC]

#16185: Add an AnonArgFlag to FunTy
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.6.3
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |  https://gitlab.haskell.org/ghc/ghc/merge_requests/128
-------------------------------------+-------------------------------------
Description changed by simonpj:

Old description:

> In Trac #15952 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:
> https://gitlab.haskell.org/ghc/ghc/merge_requests/128
>
> See [ticket:15952#comment:7] and [ticket:15952#comment:8].
>
> 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`.

New description:

 In Trac #15952 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: https://gitlab.haskell.org/ghc/ghc/merge_requests/128

 See [ticket:15952#comment:7] and [ticket:15952#comment:8].

 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.

--

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16185#comment:8>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler