Add AnonArgFlag to FunTy

The big payload of this patch is:

  Add an AnonArgFlag to the FunTy constructor
  of Type, so that
    (FunTy VisArg   t1 t2) means (t1 -> t2)
    (FunTy InvisArg t1 t2) means (t1 => t2)

The big payoff is that we have a simple, local test to make
when decomposing a type, leading to many fewer calls to
isPredTy. To me the code seems a lot tidier, and probably
more efficient (isPredTy has to take the kind of the type).

See Note [Function types] in TyCoRep.

There are lots of consequences

* I made FunTy into a record, so that it'll be easier
  when we add a linearity field, something that is coming
  down the road.

* Lots of code gets touched in a routine way, simply because it
  pattern matches on FunTy.

* I wanted to make a pattern synonym for (FunTy2 arg res), which
  picks out just the argument and result type from the record. But
  alas the pattern-match overlap checker has a heart attack, and
  either reports false positives, or takes too long.  In the end
  I gave up on pattern synonyms.

  There's some commented-out code in TyCoRep that shows what I
  wanted to do.

* Much more clarity about predicate types, constraint types
  and (in particular) equality constraints in kinds.  See TyCoRep
  Note [Types for coercions, predicates, and evidence]
  and Note [Constraints in kinds].

  This made me realise that we need an AnonArgFlag on
  AnonTCB in a TyConBinder, something that was really plain
  wrong before. See TyCon Note [AnonTCB InivsArg]

* When building function types we must know whether we
  need VisArg (mkVisFunTy) or InvisArg (mkInvisFunTy).
  This turned out to be pretty easy in practice.

* Pretty-printing of types, esp in IfaceType, gets
  tidier, because we were already recording the (->)
  vs (=>) distinction in an ad-hoc way.  Death to
  IfaceFunTy.

* mkLamType needs to keep track of whether it is building
  (t1 -> t2) or (t1 => t2).  See Type
  Note [mkLamType: dictionary arguments]

Other minor stuff

* Some tidy-up in validity checking involving constraints;
  Trac #16263

1 files changed, 3 insertions, 3 deletions

diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index 53cddbfabe..62ddb9f410 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -1349,7 +1349,7 @@ lintType ty@(TyConApp tc tys)
 
 -- arrows can related *unlifted* kinds, so this has to be separate from
 -- a dependent forall.
-lintType ty@(FunTy t1 t2)
+lintType ty@(FunTy _ t1 t2)
   = do { k1 <- lintType t1
        ; k2 <- lintType t2
        ; lintArrow (text "type or kind" <+> quotes (ppr ty)) k1 k2 }
@@ -1509,7 +1509,7 @@ lint_app doc kfn kas
       | Just kfn' <- coreView kfn
       = go_app in_scope kfn' tka
 
-    go_app _ (FunTy kfa kfb) tka@(_,ka)
+    go_app _ (FunTy _ kfa kfb) tka@(_,ka)
       = do { unless (ka `eqType` kfa) $
              addErrL (fail_msg (text "Fun:" <+> (ppr kfa $$ ppr tka)))
            ; return kfb }
@@ -1765,7 +1765,7 @@ lintCoercion co@(FunCo r co1 co2)
        ; k' <- lintArrow (text "coercion" <+> quotes (ppr co)) k'1 k'2
        ; lintRole co1 r r1
        ; lintRole co2 r r2
-       ; return (k, k', mkFunTy s1 s2, mkFunTy t1 t2, r) }
+       ; return (k, k', mkVisFunTy s1 s2, mkVisFunTy t1 t2, r) }
 
 lintCoercion (CoVarCo cv)
   | not (isCoVar cv)