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, 42 insertions, 60 deletions

diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 7fcf30a538..1f6372cd0a 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -64,7 +64,6 @@ module TcType (
   tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcFunResultTyN,
   tcSplitFunTysN,
   tcSplitTyConApp, tcSplitTyConApp_maybe,
-  tcRepSplitTyConApp, tcRepSplitTyConApp_maybe, tcRepSplitTyConApp_maybe',
   tcTyConAppTyCon, tcTyConAppTyCon_maybe, tcTyConAppArgs,
   tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcRepSplitAppTy_maybe,
   tcRepGetNumAppTys,
@@ -129,16 +128,16 @@ module TcType (
 
   --------------------------------
   -- Rexported from Type
-  Type, PredType, ThetaType, TyCoBinder, ArgFlag(..),
+  Type, PredType, ThetaType, TyCoBinder, ArgFlag(..), AnonArgFlag(..),
 
   mkForAllTy, mkForAllTys, mkTyCoInvForAllTys, mkSpecForAllTys, mkTyCoInvForAllTy,
   mkInvForAllTy, mkInvForAllTys,
-  mkFunTy, mkFunTys,
+  mkVisFunTy, mkVisFunTys, mkInvisFunTy, mkInvisFunTys,
   mkTyConApp, mkAppTy, mkAppTys,
   mkTyConTy, mkTyVarTy, mkTyVarTys,
   mkTyCoVarTy, mkTyCoVarTys,
 
-  isClassPred, isEqPred, isNomEqPred, isIPPred,
+  isClassPred, isEqPrimPred, isIPPred, isEqPred, isEqPredClass,
   mkClassPred,
   isDictLikeTy,
   tcSplitDFunTy, tcSplitDFunHead, tcSplitMethodTy,
@@ -916,7 +915,7 @@ tcTyFamInstsAndVisX = go
     go _            (LitTy {})         = []
     go is_invis_arg (ForAllTy bndr ty) = go is_invis_arg (binderType bndr)
                                          ++ go is_invis_arg ty
-    go is_invis_arg (FunTy ty1 ty2)    = go is_invis_arg ty1
+    go is_invis_arg (FunTy _ ty1 ty2)  = go is_invis_arg ty1
                                          ++ go is_invis_arg ty2
     go is_invis_arg ty@(AppTy _ _)     =
       let (ty_head, ty_args) = splitAppTys ty
@@ -983,7 +982,7 @@ exactTyCoVarsOfType ty
     go (TyConApp _ tys)     = exactTyCoVarsOfTypes tys
     go (LitTy {})           = emptyVarSet
     go (AppTy fun arg)      = go fun `unionVarSet` go arg
-    go (FunTy arg res)      = go arg `unionVarSet` go res
+    go (FunTy _ arg res)    = go arg `unionVarSet` go res
     go (ForAllTy bndr ty)   = delBinderVar (go ty) bndr `unionVarSet` go (binderType bndr)
     go (CastTy ty co)       = go ty `unionVarSet` goCo co
     go (CoercionTy co)      = goCo co
@@ -1037,14 +1036,14 @@ anyRewritableTyVar ignore_cos role pred ty
     go_tv rl bvs tv | tv `elemVarSet` bvs = False
                     | otherwise           = pred rl tv
 
-    go rl bvs (TyVarTy tv)      = go_tv rl bvs tv
-    go _ _     (LitTy {})       = False
-    go rl bvs (TyConApp tc tys) = go_tc rl bvs tc tys
-    go rl bvs (AppTy fun arg)   = go rl bvs fun || go NomEq bvs arg
-    go rl bvs (FunTy arg res)   = go rl bvs arg || go rl bvs res
-    go rl bvs (ForAllTy tv ty)  = go rl (bvs `extendVarSet` binderVar tv) ty
-    go rl bvs (CastTy ty co)    = go rl bvs ty || go_co rl bvs co
-    go rl bvs (CoercionTy co)   = go_co rl bvs co  -- ToDo: check
+    go rl bvs (TyVarTy tv)       = go_tv rl bvs tv
+    go _ _     (LitTy {})        = False
+    go rl bvs (TyConApp tc tys)  = go_tc rl bvs tc tys
+    go rl bvs (AppTy fun arg)    = go rl bvs fun || go NomEq bvs arg
+    go rl bvs (FunTy _ arg res)  = go rl bvs arg || go rl bvs res
+    go rl bvs (ForAllTy tv ty)   = go rl (bvs `extendVarSet` binderVar tv) ty
+    go rl bvs (CastTy ty co)     = go rl bvs ty || go_co rl bvs co
+    go rl bvs (CoercionTy co)    = go_co rl bvs co  -- ToDo: check
 
     go_tc NomEq  bvs _  tys = any (go NomEq bvs) tys
     go_tc ReprEq bvs tc tys = any (go_arg bvs)
@@ -1274,7 +1273,7 @@ mkSpecSigmaTy :: [TyVar] -> [PredType] -> Type -> Type
 mkSpecSigmaTy tyvars preds ty = mkSigmaTy (mkTyCoVarBinders Specified tyvars) preds ty
 
 mkPhiTy :: [PredType] -> Type -> Type
-mkPhiTy = mkFunTys
+mkPhiTy = mkInvisFunTys
 
 ---------------
 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
@@ -1284,7 +1283,7 @@ getDFunTyKey (TyVarTy tv)            = getOccName tv
 getDFunTyKey (TyConApp tc _)         = getOccName tc
 getDFunTyKey (LitTy x)               = getDFunTyLitKey x
 getDFunTyKey (AppTy fun _)           = getDFunTyKey fun
-getDFunTyKey (FunTy _ _)             = getOccName funTyCon
+getDFunTyKey (FunTy {})              = getOccName funTyCon
 getDFunTyKey (ForAllTy _ t)          = getDFunTyKey t
 getDFunTyKey (CastTy ty _)           = getDFunTyKey ty
 getDFunTyKey t@(CoercionTy _)        = pprPanic "getDFunTyKey" (ppr t)
@@ -1370,8 +1369,9 @@ tcSplitPredFunTy_maybe :: Type -> Maybe (PredType, Type)
 -- Split off the first predicate argument from a type
 tcSplitPredFunTy_maybe ty
   | Just ty' <- tcView ty = tcSplitPredFunTy_maybe ty'
-tcSplitPredFunTy_maybe (FunTy arg res)
-  | isPredTy arg = Just (arg, res)
+tcSplitPredFunTy_maybe (FunTy { ft_af = InvisArg
+                              , ft_arg = arg, ft_res = res })
+  = Just (arg, res)
 tcSplitPredFunTy_maybe _
   = Nothing
 
@@ -1414,7 +1414,7 @@ tcSplitNestedSigmaTys ty
     -- underneath it.
   | Just (arg_tys, tvs1, theta1, rho1) <- tcDeepSplitSigmaTy_maybe ty
   = let (tvs2, theta2, rho2) = tcSplitNestedSigmaTys rho1
-    in (tvs1 ++ tvs2, theta1 ++ theta2, mkFunTys arg_tys rho2)
+    in (tvs1 ++ tvs2, theta1 ++ theta2, mkVisFunTys arg_tys rho2)
     -- If there's no forall, we're done.
   | otherwise = ([], [], ty)
 
@@ -1448,8 +1448,9 @@ tcTyConAppTyCon_maybe ty
   | Just ty' <- tcView ty = tcTyConAppTyCon_maybe ty'
 tcTyConAppTyCon_maybe (TyConApp tc _)
   = Just tc
-tcTyConAppTyCon_maybe (FunTy _ _)
-  = Just funTyCon
+tcTyConAppTyCon_maybe (FunTy { ft_af = VisArg })
+  = Just funTyCon  -- (=>) is /not/ a TyCon in its own right
+                   -- C.f. tcRepSplitAppTy_maybe
 tcTyConAppTyCon_maybe _
   = Nothing
 
@@ -1463,27 +1464,6 @@ tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
                         Just stuff -> stuff
                         Nothing    -> pprPanic "tcSplitTyConApp" (pprType ty)
 
--- | Like 'tcRepSplitTyConApp_maybe', but returns 'Nothing' if,
---
--- 1. the type is structurally not a type constructor application, or
---
--- 2. the type is a function type (e.g. application of 'funTyCon'), but we
---    currently don't even enough information to fully determine its RuntimeRep
---    variables. For instance, @FunTy (a :: k) Int@.
---
--- By contrast 'tcRepSplitTyConApp_maybe' panics in the second case.
---
--- The behavior here is needed during canonicalization; see Note [FunTy and
--- decomposing tycon applications] in TcCanonical for details.
-tcRepSplitTyConApp_maybe' :: HasCallStack => Type -> Maybe (TyCon, [Type])
-tcRepSplitTyConApp_maybe' (TyConApp tc tys)          = Just (tc, tys)
-tcRepSplitTyConApp_maybe' (FunTy arg res)
-  | Just arg_rep <- getRuntimeRep_maybe arg
-  , Just res_rep <- getRuntimeRep_maybe res
-  = Just (funTyCon, [arg_rep, res_rep, arg, res])
-tcRepSplitTyConApp_maybe' _                          = Nothing
-
-
 -----------------------
 tcSplitFunTys :: Type -> ([Type], Type)
 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
@@ -1493,10 +1473,12 @@ tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
                                           (args,res') = tcSplitFunTys res
 
 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
-tcSplitFunTy_maybe ty | Just ty' <- tcView ty         = tcSplitFunTy_maybe ty'
-tcSplitFunTy_maybe (FunTy arg res) | not (isPredTy arg) = Just (arg, res)
-tcSplitFunTy_maybe _                                    = Nothing
-        -- Note the tcTypeKind guard
+tcSplitFunTy_maybe ty
+  | Just ty' <- tcView ty = tcSplitFunTy_maybe ty'
+tcSplitFunTy_maybe (FunTy { ft_af = af, ft_arg = arg, ft_res = res })
+  | VisArg <- af = Just (arg, res)
+tcSplitFunTy_maybe _ = Nothing
+        -- Note the VisArg guard
         -- Consider     (?x::Int) => Bool
         -- We don't want to treat this as a function type!
         -- A concrete example is test tc230:
@@ -1698,10 +1680,10 @@ tc_eq_type keep_syns vis_only orig_ty1 orig_ty2
     -- Make sure we handle all FunTy cases since falling through to the
     -- AppTy case means that tcRepSplitAppTy_maybe may see an unzonked
     -- kind variable, which causes things to blow up.
-    go env (FunTy arg1 res1) (FunTy arg2 res2)
+    go env (FunTy _ arg1 res1) (FunTy _ arg2 res2)
       = go env arg1 arg2 && go env res1 res2
-    go env ty (FunTy arg res) = eqFunTy env arg res ty
-    go env (FunTy arg res) ty = eqFunTy env arg res ty
+    go env ty (FunTy _ arg res) = eqFunTy env arg res ty
+    go env (FunTy _ arg res) ty = eqFunTy env arg res ty
 
       -- See Note [Equality on AppTys] in Type
     go env (AppTy s1 t1)        ty2
@@ -2001,7 +1983,7 @@ isInsolubleOccursCheck eq_rel tv ty
     go (AppTy t1 t2) = case eq_rel of  -- See Note [AppTy and ReprEq]
                          NomEq  -> go t1 || go t2
                          ReprEq -> go t1
-    go (FunTy t1 t2) = go t1 || go t2
+    go (FunTy _ t1 t2) = go t1 || go t2
     go (ForAllTy (Bndr tv' _) inner_ty)
       | tv' == tv = False
       | otherwise = go (varType tv') || go inner_ty
@@ -2121,15 +2103,15 @@ isSigmaTy :: TcType -> Bool
 -- *necessarily* have any foralls.  E.g
 --        f :: (?x::Int) => Int -> Int
 isSigmaTy ty | Just ty' <- tcView ty = isSigmaTy ty'
-isSigmaTy (ForAllTy {}) = True
-isSigmaTy (FunTy a _)   = isPredTy a
-isSigmaTy _             = False
+isSigmaTy (ForAllTy {})                = True
+isSigmaTy (FunTy { ft_af = InvisArg }) = True
+isSigmaTy _                            = False
 
 isRhoTy :: TcType -> Bool   -- True of TcRhoTypes; see Note [TcRhoType]
 isRhoTy ty | Just ty' <- tcView ty = isRhoTy ty'
-isRhoTy (ForAllTy {}) = False
-isRhoTy (FunTy a r)   = not (isPredTy a) && isRhoTy r
-isRhoTy _             = True
+isRhoTy (ForAllTy {})                          = False
+isRhoTy (FunTy { ft_af = VisArg, ft_res = r }) = isRhoTy r
+isRhoTy _                                      = True
 
 -- | Like 'isRhoTy', but also says 'True' for 'Infer' types
 isRhoExpTy :: ExpType -> Bool
@@ -2140,9 +2122,9 @@ isOverloadedTy :: Type -> Bool
 -- Yes for a type of a function that might require evidence-passing
 -- Used only by bindLocalMethods
 isOverloadedTy ty | Just ty' <- tcView ty = isOverloadedTy ty'
-isOverloadedTy (ForAllTy _  ty) = isOverloadedTy ty
-isOverloadedTy (FunTy a _)      = isPredTy a
-isOverloadedTy _                = False
+isOverloadedTy (ForAllTy _  ty)             = isOverloadedTy ty
+isOverloadedTy (FunTy { ft_af = InvisArg }) = True
+isOverloadedTy _                            = False
 
 isFloatTy, isDoubleTy, isIntegerTy, isIntTy, isWordTy, isBoolTy,
     isUnitTy, isCharTy, isAnyTy :: Type -> Bool
@@ -2570,7 +2552,7 @@ sizeType = go
                                    -- size ordering is sound, but why is this better?
                                    -- I came across this when investigating #14010.
     go (LitTy {})                = 1
-    go (FunTy arg res)           = go arg + go res + 1
+    go (FunTy _ arg res)         = go arg + go res + 1
     go (AppTy fun arg)           = go fun + go arg
     go (ForAllTy (Bndr tv vis) ty)
         | isVisibleArgFlag vis   = go (tyVarKind tv) + go ty + 1