Add AnonArgFlag to FunTy
authorSimon Peyton Jones <simonpj@microsoft.com>
Fri, 15 Feb 2019 09:53:48 +0000 (09:53 +0000)
committerMarge Bot <ben+marge-bot@smart-cactus.org>
Sun, 24 Feb 2019 02:31:47 +0000 (21:31 -0500)
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

83 files changed:
compiler/backpack/RnModIface.hs
compiler/basicTypes/DataCon.hs
compiler/basicTypes/MkId.hs
compiler/basicTypes/PatSyn.hs
compiler/basicTypes/Var.hs
compiler/basicTypes/Var.hs-boot [new file with mode: 0644]
compiler/codeGen/StgCmmClosure.hs
compiler/coreSyn/CoreFVs.hs
compiler/coreSyn/CoreLint.hs
compiler/coreSyn/CoreMap.hs
compiler/coreSyn/CoreUtils.hs
compiler/coreSyn/MkCore.hs
compiler/deSugar/DsCCall.hs
compiler/deSugar/DsForeign.hs
compiler/deSugar/DsListComp.hs
compiler/deSugar/DsUtils.hs
compiler/ghci/ByteCodeGen.hs
compiler/ghci/RtClosureInspect.hs
compiler/hieFile/HieAst.hs
compiler/hieFile/HieUtils.hs
compiler/hsSyn/HsUtils.hs
compiler/iface/BuildTyCl.hs
compiler/iface/IfaceSyn.hs
compiler/iface/IfaceType.hs
compiler/iface/TcIface.hs
compiler/iface/ToIface.hs
compiler/prelude/PrimOp.hs
compiler/prelude/TysPrim.hs
compiler/prelude/TysWiredIn.hs
compiler/prelude/TysWiredIn.hs-boot
compiler/simplCore/SimplUtils.hs
compiler/simplStg/RepType.hs
compiler/typecheck/ClsInst.hs
compiler/typecheck/FamInst.hs
compiler/typecheck/Inst.hs
compiler/typecheck/TcArrows.hs
compiler/typecheck/TcCanonical.hs
compiler/typecheck/TcDerivInfer.hs
compiler/typecheck/TcErrors.hs
compiler/typecheck/TcEvidence.hs
compiler/typecheck/TcExpr.hs
compiler/typecheck/TcFlatten.hs
compiler/typecheck/TcForeign.hs
compiler/typecheck/TcGenDeriv.hs
compiler/typecheck/TcGenFunctor.hs
compiler/typecheck/TcHoleErrors.hs
compiler/typecheck/TcHsType.hs
compiler/typecheck/TcInstDcls.hs
compiler/typecheck/TcMType.hs
compiler/typecheck/TcMatches.hs
compiler/typecheck/TcPat.hs
compiler/typecheck/TcPatSyn.hs
compiler/typecheck/TcRnDriver.hs
compiler/typecheck/TcRnTypes.hs
compiler/typecheck/TcSMonad.hs
compiler/typecheck/TcSigs.hs
compiler/typecheck/TcSimplify.hs
compiler/typecheck/TcSplice.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/typecheck/TcTyDecls.hs
compiler/typecheck/TcType.hs
compiler/typecheck/TcTypeable.hs
compiler/typecheck/TcUnify.hs
compiler/typecheck/TcValidity.hs
compiler/types/Coercion.hs
compiler/types/FamInstEnv.hs
compiler/types/Kind.hs
compiler/types/OptCoercion.hs
compiler/types/TyCoRep.hs
compiler/types/TyCoRep.hs-boot
compiler/types/TyCon.hs
compiler/types/Type.hs
compiler/types/Unify.hs
docs/users_guide/glasgow_exts.rst
testsuite/tests/callarity/unittest/CallArity1.hs
testsuite/tests/dependent/should_fail/T15215.hs
testsuite/tests/dependent/should_fail/T15215.stderr
testsuite/tests/polykinds/all.T
testsuite/tests/typecheck/should_fail/T12102.hs
testsuite/tests/typecheck/should_fail/T12102.stderr [deleted file]
testsuite/tests/typecheck/should_fail/all.T
utils/genprimopcode/Main.hs
utils/haddock

index 01cf47f..af24fcc 100644 (file)
@@ -721,10 +721,8 @@ rnIfaceType (IfaceTyVar   n)   = pure (IfaceTyVar n)
 rnIfaceType (IfaceAppTy t1 t2)
     = IfaceAppTy <$> rnIfaceType t1 <*> rnIfaceAppArgs t2
 rnIfaceType (IfaceLitTy l)         = return (IfaceLitTy l)
-rnIfaceType (IfaceFunTy t1 t2)
-    = IfaceFunTy <$> rnIfaceType t1 <*> rnIfaceType t2
-rnIfaceType (IfaceDFunTy t1 t2)
-    = IfaceDFunTy <$> rnIfaceType t1 <*> rnIfaceType t2
+rnIfaceType (IfaceFunTy af t1 t2)
+    = IfaceFunTy af <$> rnIfaceType t1 <*> rnIfaceType t2
 rnIfaceType (IfaceTupleTy s i tks)
     = IfaceTupleTy s i <$> rnIfaceAppArgs tks
 rnIfaceType (IfaceTyConApp tc tks)
index f34a6cb..8baf43c 100644 (file)
@@ -959,36 +959,33 @@ mkDataCon name declared_infix prom_info
         -- If the DataCon has a wrapper, then the worker's type is never seen
         -- by the user. The visibilities we pick do not matter here.
         DCR{} -> mkInvForAllTys univ_tvs $ mkTyCoInvForAllTys ex_tvs $
-                 mkFunTys rep_arg_tys $
+                 mkVisFunTys rep_arg_tys $
                  mkTyConApp rep_tycon (mkTyVarTys univ_tvs)
 
       -- See Note [Promoted data constructors] in TyCon
     prom_tv_bndrs = [ mkNamedTyConBinder vis tv
                     | Bndr tv vis <- user_tvbs ]
 
-    prom_arg_bndrs = mkCleanAnonTyConBinders prom_tv_bndrs (theta ++ orig_arg_tys)
-    prom_res_kind  = orig_res_ty
-    promoted       = mkPromotedDataCon con name prom_info
-                                       (prom_tv_bndrs ++ prom_arg_bndrs)
-                                       prom_res_kind roles rep_info
+    fresh_names = freshNames (map getName user_tvbs)
+      -- fresh_names: make sure that the "anonymous" tyvars don't
+      -- clash in name or unique with the universal/existential ones.
+      -- Tiresome!  And unnecessary because these tyvars are never looked at
+    prom_theta_bndrs = [ mkAnonTyConBinder InvisArg (mkTyVar n t)
+     {- Invisible -}   | (n,t) <- fresh_names `zip` theta ]
+    prom_arg_bndrs   = [ mkAnonTyConBinder VisArg (mkTyVar n t)
+     {- Visible -}     | (n,t) <- dropList theta fresh_names `zip` orig_arg_tys ]
+    prom_bndrs       = prom_tv_bndrs ++ prom_theta_bndrs ++ prom_arg_bndrs
+    prom_res_kind    = orig_res_ty
+    promoted         = mkPromotedDataCon con name prom_info prom_bndrs
+                                         prom_res_kind roles rep_info
 
     roles = map (\tv -> if isTyVar tv then Nominal else Phantom)
                 (univ_tvs ++ ex_tvs)
-            ++ map (const Representational) orig_arg_tys
-
-mkCleanAnonTyConBinders :: [TyConBinder] -> [Type] -> [TyConBinder]
--- Make sure that the "anonymous" tyvars don't clash in
--- name or unique with the universal/existential ones.
--- Tiresome!  And unnecessary because these tyvars are never looked at
-mkCleanAnonTyConBinders tc_bndrs tys
-  = [ mkAnonTyConBinder (mkTyVar name ty)
-    | (name, ty) <- fresh_names `zip` tys ]
-  where
-    fresh_names = freshNames (map getName (binderVars tc_bndrs))
+            ++ map (const Representational) (theta ++ orig_arg_tys)
 
 freshNames :: [Name] -> [Name]
--- Make names whose Uniques and OccNames differ from
--- those in the 'avoid' list
+-- Make an infinite list of Names whose Uniques and OccNames
+-- differ from those in the 'avoid' list
 freshNames avoids
   = [ mkSystemName uniq occ
     | n <- [0..]
@@ -1299,8 +1296,8 @@ dataConUserType (MkData { dcUserTyVarBinders = user_tvbs,
                           dcOtherTheta = theta, dcOrigArgTys = arg_tys,
                           dcOrigResTy = res_ty })
   = mkForAllTys user_tvbs $
-    mkFunTys theta $
-    mkFunTys arg_tys $
+    mkInvisFunTys theta $
+    mkVisFunTys arg_tys $
     res_ty
 
 -- | Finds the instantiated types of the arguments required to construct a
index 1802cd7..ceda502 100644 (file)
@@ -337,7 +337,7 @@ mkDictSelId name clas
     val_index      = assoc "MkId.mkDictSelId" (sel_names `zip` [0..]) name
 
     sel_ty = mkForAllTys tyvars $
-             mkFunTy (mkClassPred clas (mkTyVarTys (binderVars tyvars))) $
+             mkInvisFunTy (mkClassPred clas (mkTyVarTys (binderVars tyvars))) $
              getNth arg_tys val_index
 
     base_info = noCafIdInfo
@@ -1137,7 +1137,7 @@ mkPrimOpId prim_op
   = id
   where
     (tyvars,arg_tys,res_ty, arity, strict_sig) = primOpSig prim_op
-    ty   = mkSpecForAllTys tyvars (mkFunTys arg_tys res_ty)
+    ty   = mkSpecForAllTys tyvars (mkVisFunTys arg_tys res_ty)
     name = mkWiredInName gHC_PRIM (primOpOcc prim_op)
                          (mkPrimOpIdUnique (primOpTag prim_op))
                          (AnId id) UserSyntax
@@ -1297,7 +1297,7 @@ unsafeCoerceId
 
     [_, _, a, b] = mkTyVarTys bndrs
 
-    ty  = mkSpecForAllTys bndrs (mkFunTy a b)
+    ty  = mkSpecForAllTys bndrs (mkVisFunTy a b)
 
     [x] = mkTemplateLocals [a]
     rhs = mkLams (bndrs ++ [x]) $
@@ -1331,7 +1331,7 @@ seqId = pcMiscPrelId seqName ty info
                   -- see Note [seqId magic]
 
     ty  = mkSpecForAllTys [alphaTyVar,betaTyVar]
-                          (mkFunTy alphaTy (mkFunTy betaTy betaTy))
+                          (mkVisFunTy alphaTy (mkVisFunTy betaTy betaTy))
 
     [x,y] = mkTemplateLocals [alphaTy, betaTy]
     rhs = mkLams [alphaTyVar,betaTyVar,x,y] (Case (Var x) x betaTy [(DEFAULT, [], Var y)])
@@ -1341,13 +1341,13 @@ lazyId :: Id    -- See Note [lazyId magic]
 lazyId = pcMiscPrelId lazyIdName ty info
   where
     info = noCafIdInfo `setNeverLevPoly` ty
-    ty  = mkSpecForAllTys [alphaTyVar] (mkFunTy alphaTy alphaTy)
+    ty  = mkSpecForAllTys [alphaTyVar] (mkVisFunTy alphaTy alphaTy)
 
 noinlineId :: Id -- See Note [noinlineId magic]
 noinlineId = pcMiscPrelId noinlineIdName ty info
   where
     info = noCafIdInfo `setNeverLevPoly` ty
-    ty  = mkSpecForAllTys [alphaTyVar] (mkFunTy alphaTy alphaTy)
+    ty  = mkSpecForAllTys [alphaTyVar] (mkVisFunTy alphaTy alphaTy)
 
 oneShotId :: Id -- See Note [The oneShot function]
 oneShotId = pcMiscPrelId oneShotName ty info
@@ -1356,8 +1356,8 @@ oneShotId = pcMiscPrelId oneShotName ty info
                        `setUnfoldingInfo`  mkCompulsoryUnfolding rhs
     ty  = mkSpecForAllTys [ runtimeRep1TyVar, runtimeRep2TyVar
                           , openAlphaTyVar, openBetaTyVar ]
-                          (mkFunTy fun_ty fun_ty)
-    fun_ty = mkFunTy openAlphaTy openBetaTy
+                          (mkVisFunTy fun_ty fun_ty)
+    fun_ty = mkVisFunTy openAlphaTy openBetaTy
     [body, x] = mkTemplateLocals [fun_ty, openAlphaTy]
     x' = setOneShotLambda x  -- Here is the magic bit!
     rhs = mkLams [ runtimeRep1TyVar, runtimeRep2TyVar
@@ -1387,7 +1387,8 @@ coerceId = pcMiscPrelId coerceName ty info
                                            , liftedTypeKind
                                            , alphaTy, betaTy ]
     ty        = mkSpecForAllTys [alphaTyVar, betaTyVar] $
-                mkFunTys [eqRTy, alphaTy] betaTy
+                mkInvisFunTy eqRTy                      $
+                mkVisFunTy alphaTy betaTy
 
     [eqR,x,eq] = mkTemplateLocals [eqRTy, alphaTy, eqRPrimTy]
     rhs = mkLams [alphaTyVar, betaTyVar, eqR, x] $
index bf9426e..2f8cee4 100644 (file)
@@ -464,6 +464,6 @@ pprPatSynType (MkPatSyn { psUnivTyVars = univ_tvs,  psReqTheta  = req_theta
         , pprType sigma_ty ]
   where
     sigma_ty = mkForAllTys ex_tvs  $
-               mkFunTys prov_theta $
-               mkFunTys orig_args orig_res_ty
+               mkInvisFunTys prov_theta $
+               mkVisFunTys orig_args orig_res_ty
     insert_empty_ctxt = null req_theta && not (null prov_theta && null ex_tvs)
index bfa5e5f..7e451e5 100644 (file)
@@ -60,10 +60,13 @@ module Var (
         isGlobalId, isExportedId,
         mustHaveLocalBinding,
 
+        -- * ArgFlags
+        ArgFlag(..), isVisibleArgFlag, isInvisibleArgFlag, sameVis,
+        AnonArgFlag(..),
+
         -- * TyVar's
-        VarBndr(..), ArgFlag(..), TyCoVarBinder, TyVarBinder,
+        VarBndr(..), TyCoVarBinder, TyVarBinder,
         binderVar, binderVars, binderArgFlag, binderType,
-        isVisibleArgFlag, isInvisibleArgFlag, sameVis,
         mkTyCoVarBinder, mkTyCoVarBinders,
         mkTyVarBinder, mkTyVarBinders,
         isTyVarBinder,
@@ -422,6 +425,31 @@ instance Binary ArgFlag where
       1 -> return Specified
       _ -> return Inferred
 
+-- The non-dependent version of ArgFlag, namely AnonArgFlag,
+-- appears here partly so that it's together with its friend ArgFlag,
+-- but also because it is used in IfaceType, rather early in the
+-- compilation chain
+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
+  deriving (Eq, Ord, Data)
+
+instance Outputable AnonArgFlag where
+  ppr VisArg   = text "[vis]"
+  ppr InvisArg = text "[invis]"
+
+instance Binary AnonArgFlag where
+  put_ bh VisArg   = putByte bh 0
+  put_ bh InvisArg = putByte bh 1
+
+  get bh = do
+    h <- getByte bh
+    case h of
+      0 -> return VisArg
+      _ -> return InvisArg
+
 {- *********************************************************************
 *                                                                      *
 *                   VarBndr, TyCoVarBinder
diff --git a/compiler/basicTypes/Var.hs-boot b/compiler/basicTypes/Var.hs-boot
new file mode 100644 (file)
index 0000000..aa022ea
--- /dev/null
@@ -0,0 +1,15 @@
+-- Var.hs-boot is Imported (only) by TyCoRep.hs-boot
+module Var where
+
+import GhcPrelude ()
+  -- We compile this module with -XNoImplicitPrelude (for some
+  -- reason), so if there are no imports it does not seem to
+  -- depend on anything.  But it does! We must, for example,
+  -- compile GHC.Types in the ghc-prim library first.
+  -- So this otherwise-unnecessary import tells the build system
+  -- that this module depends on GhcPrelude, which ensures
+  -- that GHC.Type is built first.
+
+data ArgFlag
+data AnonArgFlag
+data Var
index 8ad8951..8a32a7f 100644 (file)
@@ -928,15 +928,15 @@ getTyDescription ty
       TyVarTy _              -> "*"
       AppTy fun _            -> getTyDescription fun
       TyConApp tycon _       -> getOccString tycon
-      FunTy _ res            -> '-' : '>' : fun_result res
+      FunTy {}              -> '-' : fun_result tau_ty
       ForAllTy _  ty         -> getTyDescription ty
       LitTy n                -> getTyLitDescription n
       CastTy ty _            -> getTyDescription ty
       CoercionTy co          -> pprPanic "getTyDescription" (ppr co)
     }
   where
-    fun_result (FunTy _ res) = '>' : fun_result res
-    fun_result other         = getTyDescription other
+    fun_result (FunTy { ft_res = res }) = '>' : fun_result res
+    fun_result other                    = getTyDescription other
 
 getTyLitDescription :: TyLit -> String
 getTyLitDescription l =
index bc54d26..18e109a 100644 (file)
@@ -353,7 +353,7 @@ orphNamesOfType (TyConApp tycon tys) = orphNamesOfTyCon tycon
                                        `unionNameSet` orphNamesOfTypes tys
 orphNamesOfType (ForAllTy bndr res)  = orphNamesOfType (binderType bndr)
                                        `unionNameSet` orphNamesOfType res
-orphNamesOfType (FunTy arg res)      = unitNameSet funTyConName    -- NB!  See Trac #8535
+orphNamesOfType (FunTy _ arg res)    = unitNameSet funTyConName    -- NB!  See Trac #8535
                                        `unionNameSet` orphNamesOfType arg
                                        `unionNameSet` orphNamesOfType res
 orphNamesOfType (AppTy fun arg)      = orphNamesOfType fun `unionNameSet` orphNamesOfType arg
index 53cddbf..62ddb9f 100644 (file)
@@ -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)
index 11f2fb1..3d06934 100644 (file)
@@ -3,12 +3,14 @@
 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 -}
 
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE TypeSynonymInstances #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE UndecidableInstances #-}
+
 module CoreMap(
    -- * Maps over Core expressions
    CoreMap, emptyCoreMap, extendCoreMap, lookupCoreMap, foldCoreMap,
@@ -33,6 +35,8 @@ module CoreMap(
    (>.>), (|>), (|>>),
  ) where
 
+#include "HsVersions.h"
+
 import GhcPrelude
 
 import TrieMap
@@ -516,7 +520,7 @@ instance Eq (DeBruijn Type) where
             -> D env t1 == D env' t1' && D env t2 == D env' t2'
         (s, AppTy t1' t2') | Just (t1, t2) <- repSplitAppTy_maybe s
             -> D env t1 == D env' t1' && D env t2 == D env' t2'
-        (FunTy t1 t2, FunTy t1' t2')
+        (FunTy _ t1 t2, FunTy _ t1' t2')
             -> D env t1 == D env' t1' && D env t2 == D env' t2'
         (TyConApp tc tys, TyConApp tc' tys')
             -> tc == tc' && D env tys == D env' tys'
index 4602dfa..ee79a0f 100644 (file)
@@ -1380,9 +1380,10 @@ isExpandableApp fn n_val_args
        = True
 
        | Just (bndr, ty) <- splitPiTy_maybe ty
-       = caseBinder bndr
-           (\_tv -> all_pred_args n_val_args ty)
-           (\bndr_ty -> isPredTy bndr_ty && all_pred_args (n_val_args-1) ty)
+       = case bndr of
+           Named {}        -> all_pred_args n_val_args ty
+           Anon InvisArg _ -> all_pred_args (n_val_args-1) ty
+           Anon VisArg _   -> False
 
        | otherwise
        = False
@@ -1578,7 +1579,7 @@ app_ok primop_ok fun args
 
     primop_arg_ok :: TyBinder -> CoreExpr -> Bool
     primop_arg_ok (Named _) _ = True   -- A type argument
-    primop_arg_ok (Anon ty) arg        -- A term argument
+    primop_arg_ok (Anon _ ty) arg      -- A term argument
        | isUnliftedType ty = expr_ok primop_ok arg
        | otherwise         = True  -- See Note [Primops with lifted arguments]
 
index 1583c59..999cfc7 100644 (file)
@@ -622,7 +622,7 @@ mkBuildExpr :: (MonadFail.MonadFail m, MonadThings m, MonadUnique m)
 mkBuildExpr elt_ty mk_build_inside = do
     [n_tyvar] <- newTyVars [alphaTyVar]
     let n_ty = mkTyVarTy n_tyvar
-        c_ty = mkFunTys [elt_ty, n_ty] n_ty
+        c_ty = mkVisFunTys [elt_ty, n_ty] n_ty
     [c, n] <- sequence [mkSysLocalM (fsLit "c") c_ty, mkSysLocalM (fsLit "n") n_ty]
 
     build_inside <- mk_build_inside (c, c_ty) (n, n_ty)
@@ -804,7 +804,7 @@ runtimeErrorTy :: Type
 -- forall (rr :: RuntimeRep) (a :: rr). Addr# -> a
 --   See Note [Error and friends have an "open-tyvar" forall]
 runtimeErrorTy = mkSpecForAllTys [runtimeRep1TyVar, openAlphaTyVar]
-                                 (mkFunTy addrPrimTy openAlphaTy)
+                                 (mkVisFunTy addrPrimTy openAlphaTy)
 
 {- Note [Error and friends have an "open-tyvar" forall]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -894,7 +894,7 @@ be relying on anything from it.
 aBSENT_ERROR_ID
  = mkVanillaGlobalWithInfo absentErrorName absent_ty arity_info
  where
-   absent_ty = mkSpecForAllTys [alphaTyVar] (mkFunTy addrPrimTy alphaTy)
+   absent_ty = mkSpecForAllTys [alphaTyVar] (mkVisFunTy addrPrimTy alphaTy)
    -- Not runtime-rep polymorphic. aBSENT_ERROR_ID is only used for
    -- lifted-type things; see Note [Absent errors] in WwLib
    arity_info = vanillaIdInfo `setArityInfo` 1
index 7cab8e8..3df8ee1 100644 (file)
@@ -120,7 +120,7 @@ mkFCall dflags uniq the_fcall val_args res_ty
     mkApps (mkVarApps (Var the_fcall_id) tyvars) val_args
   where
     arg_tys = map exprType val_args
-    body_ty = (mkFunTys arg_tys res_ty)
+    body_ty = (mkVisFunTys arg_tys res_ty)
     tyvars  = tyCoVarsOfTypeWellScoped body_ty
     ty      = mkInvForAllTys tyvars body_ty
     the_fcall_id = mkFCallId dflags uniq the_fcall ty
@@ -251,7 +251,7 @@ boxResult result_ty
                                              [the_alt]
                                      ]
 
-        ; return (realWorldStatePrimTy `mkFunTy` ccall_res_ty, wrap) }
+        ; return (realWorldStatePrimTy `mkVisFunTy` ccall_res_ty, wrap) }
 
 boxResult result_ty
   = do -- It isn't IO, so do unsafePerformIO
@@ -263,7 +263,7 @@ boxResult result_ty
                                            ccall_res_ty
                                            (coreAltType the_alt)
                                            [the_alt]
-       return (realWorldStatePrimTy `mkFunTy` ccall_res_ty, wrap)
+       return (realWorldStatePrimTy `mkVisFunTy` ccall_res_ty, wrap)
   where
     return_result _ [ans] = ans
     return_result _ _     = panic "return_result: expected single result"
index d34c3a7..95a5e4a 100644 (file)
@@ -271,7 +271,7 @@ dsFCall fn_id co fcall mDeclHeader = do
                   return (fcall, empty)
     let
         -- Build the worker
-        worker_ty     = mkForAllTys tv_bndrs (mkFunTys (map idType work_arg_ids) ccall_result_ty)
+        worker_ty     = mkForAllTys tv_bndrs (mkVisFunTys (map idType work_arg_ids) ccall_result_ty)
         tvs           = map binderVar tv_bndrs
         the_ccall_app = mkFCall dflags ccall_uniq fcall' val_args ccall_result_ty
         work_rhs      = mkLams tvs (mkLams work_arg_ids the_ccall_app)
@@ -431,7 +431,7 @@ dsFExportDynamic id co0 cconv = do
     stable_ptr_tycon <- dsLookupTyCon stablePtrTyConName
     let
         stable_ptr_ty = mkTyConApp stable_ptr_tycon [arg_ty]
-        export_ty     = mkFunTy stable_ptr_ty arg_ty
+        export_ty     = mkVisFunTy stable_ptr_ty arg_ty
     bindIOId <- dsLookupGlobalId bindIOName
     stbl_value <- newSysLocalDs stable_ptr_ty
     (h_code, c_code, typestring, args_size) <- dsFExport id (mkRepReflCo export_ty) fe_nm cconv True
index def390c..f376ef0 100644 (file)
@@ -282,7 +282,7 @@ deBindComp pat core_list1 quals core_list2 = do
     let u2_ty = hsLPatType pat
 
     let res_ty = exprType core_list2
-        h_ty   = u1_ty `mkFunTy` res_ty
+        h_ty   = u1_ty `mkVisFunTy` res_ty
 
        -- no levity polymorphism here, as list comprehensions don't work
        -- with RebindableSyntax. NB: These are *not* monad comps.
@@ -425,7 +425,7 @@ mkZipBind elt_tys = do
     elt_tuple_ty      = mkBigCoreTupTy elt_tys
     elt_tuple_list_ty = mkListTy elt_tuple_ty
 
-    zip_fn_ty         = mkFunTys elt_list_tys elt_tuple_list_ty
+    zip_fn_ty         = mkVisFunTys elt_list_tys elt_tuple_list_ty
 
     mk_case (as, a', as') rest
           = Case (Var as) as elt_tuple_list_ty
@@ -473,7 +473,7 @@ mkUnzipBind _ elt_tys
     elt_list_tys       = map mkListTy elt_tys
     elt_list_tuple_ty  = mkBigCoreTupTy elt_list_tys
 
-    unzip_fn_ty        = elt_tuple_list_ty `mkFunTy` elt_list_tuple_ty
+    unzip_fn_ty        = elt_tuple_list_ty `mkVisFunTy` elt_list_tuple_ty
 
     mkConcatExpression (list_element_ty, head, tail) = mkConsExpr list_element_ty head tail
 
index b78eef4..f39d0f2 100644 (file)
@@ -849,7 +849,7 @@ mkFailurePair :: CoreExpr       -- Result type of the whole case expression
                       CoreExpr) -- Fail variable applied to realWorld#
 -- See Note [Failure thunks and CPR]
 mkFailurePair expr
-  = do { fail_fun_var <- newFailLocalDs (voidPrimTy `mkFunTy` ty)
+  = do { fail_fun_var <- newFailLocalDs (voidPrimTy `mkVisFunTy` ty)
        ; fail_fun_arg <- newSysLocalDs voidPrimTy
        ; let real_arg = setOneShotLambda fail_fun_arg
        ; return (NonRec fail_fun_var (Lam real_arg expr),
index 1136907..86bb72b 100644 (file)
@@ -623,7 +623,7 @@ schemeE d s p exp@(AnnTick (Breakpoint _id _fvs) _rhs)
           -- Here (k n) :: a :: Type r, so we don't know if it's lifted
           -- or not; but that should be fine provided we add that void arg.
 
-          id <- newId (mkFunTy realWorldStatePrimTy ty)
+          id <- newId (mkVisFunTy realWorldStatePrimTy ty)
           st <- newId realWorldStatePrimTy
           let letExp = AnnLet (AnnNonRec id (fvs, AnnLam st (emptyDVarSet, exp)))
                               (emptyDVarSet, (AnnApp (emptyDVarSet, AnnVar id)
index 4a119a9..82e0f88 100644 (file)
@@ -752,9 +752,9 @@ cvObtainTerm hsc_env max_depth force old_ty hval = runTR hsc_env $ do
          traceTR (text "Following a MutVar")
          contents_tv <- newVar liftedTypeKind
          MASSERT(isUnliftedType my_ty)
-         (mutvar_ty,_) <- instScheme $ quantifyType $ mkFunTy
+         (mutvar_ty,_) <- instScheme $ quantifyType $ mkVisFunTy
                             contents_ty (mkTyConApp tycon [world,contents_ty])
-         addConstraint (mkFunTy contents_tv my_ty) mutvar_ty
+         addConstraint (mkVisFunTy contents_tv my_ty) mutvar_ty
          x <- go (pred max_depth) contents_tv contents_ty contents
          return (RefWrap my_ty x)
 
@@ -1259,7 +1259,7 @@ congruenceNewtypes lhs rhs = go lhs rhs >>= \rhs' -> return (lhs,rhs')
     , Just (r1,r2) <- splitFunTy_maybe r
     = do r2' <- go l2 r2
          r1' <- go l1 r1
-         return (mkFunTy r1' r2')
+         return (mkVisFunTy r1' r2')
 -- TyconApp Inductive case; this is the interesting bit.
     | Just (tycon_l, _) <- tcSplitTyConApp_maybe lhs
     , Just (tycon_r, _) <- tcSplitTyConApp_maybe rhs
index 7fd217c..9ac65ce 100644 (file)
@@ -31,7 +31,7 @@ import Name                       ( Name, nameSrcSpan, setNameLoc )
 import NameEnv                    ( NameEnv, emptyNameEnv, extendNameEnv, lookupNameEnv )
 import SrcLoc
 import TcHsSyn                    ( hsLitType, hsPatType )
-import Type                       ( mkFunTys, Type )
+import Type                       ( mkVisFunTys, Type )
 import TysWiredIn                 ( mkListTy, mkSumTy )
 import Var                        ( Id, Var, setVarName, varName, varType )
 import TcRnTypes
@@ -488,7 +488,7 @@ instance HasType (LHsExpr GhcTc) where
       fallback = makeNode e' spn
 
       matchGroupType :: MatchGroupTc -> Type
-      matchGroupType (MatchGroupTc args res) = mkFunTys args res
+      matchGroupType (MatchGroupTc args res) = mkVisFunTys args res
 
       -- | Skip desugaring of these expressions for performance reasons.
       --
index 5259ea1..9231317 100644 (file)
@@ -63,7 +63,7 @@ resolveVisibility kind ty_args
       where
         ts' = go (extendTvSubst env tv t) res ts
 
-    go env (FunTy _ res) (t:ts) -- No type-class args in tycon apps
+    go env (FunTy { ft_res = res }) (t:ts) -- No type-class args in tycon apps
       = (True,t) : (go env res ts)
 
     go env (TyVarTy tv) ts
@@ -81,8 +81,8 @@ hieTypeToIface = foldType go
     go (HLitTy l) = IfaceLitTy l
     go (HForAllTy ((n,k),af) t) = let b = (occNameFS $ getOccName n, k)
                                   in IfaceForAllTy (Bndr (IfaceTvBndr b) af) t
-    go (HFunTy a b) = IfaceFunTy a b
-    go (HQualTy pred b) = IfaceDFunTy pred b
+    go (HFunTy a b)     = IfaceFunTy VisArg   a    b
+    go (HQualTy pred b) = IfaceFunTy InvisArg pred b
     go (HCastTy a) = a
     go HCoercionTy = IfaceTyVar "<coercion type>"
     go (HTyConApp a xs) = IfaceTyConApp a (hieToIfaceArgs xs)
@@ -158,12 +158,12 @@ getTypeIndex t
       k <- getTypeIndex (varType v)
       i <- getTypeIndex t
       return $ HForAllTy ((varName v,k),a) i
-    go (FunTy a b) = do
+    go (FunTy { ft_af = af, ft_arg = a, ft_res = b }) = do
       ai <- getTypeIndex a
       bi <- getTypeIndex b
-      return $ if isPredTy a
-                  then HQualTy ai bi
-                  else HFunTy ai bi
+      return $ case af of
+                 InvisArg -> HQualTy ai bi
+                 VisArg   -> HFunTy ai bi
     go (LitTy a) = return $ HLitTy $ toIfaceTyLit a
     go (CastTy t _) = do
       i <- getTypeIndex t
index 72c70a8..7d7ad44 100644 (file)
@@ -645,13 +645,14 @@ typeToLHsType ty
   = go ty
   where
     go :: Type -> LHsType GhcPs
-    go ty@(FunTy arg _)
-      | isPredTy arg
-      , (theta, tau) <- tcSplitPhiTy ty
-      = noLoc (HsQualTy { hst_ctxt = noLoc (map go theta)
-                        , hst_xqual = noExt
-                        , hst_body = go tau })
-    go (FunTy arg res) = nlHsFunTy (go arg) (go res)
+    go ty@(FunTy { ft_af = af, ft_arg = arg, ft_res = res })
+      = case af of
+          VisArg   -> nlHsFunTy (go arg) (go res)
+          InvisArg | (theta, tau) <- tcSplitPhiTy ty
+                   -> noLoc (HsQualTy { hst_ctxt = noLoc (map go theta)
+                                      , hst_xqual = noExt
+                                      , hst_body = go tau })
+
     go ty@(ForAllTy {})
       | (tvs, tau) <- tcSplitForAllTys ty
       = noLoc (HsForAllTy { hst_bndrs = map go_tv tvs
index 693e289..4cbcb96 100644 (file)
@@ -247,8 +247,7 @@ buildClass tycon_name binders roles fds Nothing
     do  { traceIf (text "buildClass")
 
         ; tc_rep_name  <- newTyConRepName tycon_name
-        ; let univ_bndrs = tyConTyVarBinders binders
-              univ_tvs   = binderVars univ_bndrs
+        ; let univ_tvs = binderVars binders
               tycon = mkClassTyCon tycon_name binders roles
                                    AbstractTyCon rec_clas tc_rep_name
               result = mkAbstractClass tycon_name univ_tvs fds tycon
index 3dd8a21..05f64df 100644 (file)
@@ -882,7 +882,7 @@ pprIfaceDecl _ (IfacePatSyn { ifName = name,
                              , ppWhen insert_empty_ctxt $ parens empty <+> darrow
                              , ex_msg
                              , pprIfaceContextArr prov_ctxt
-                             , pprIfaceType $ foldr IfaceFunTy pat_ty arg_tys ])
+                             , pprIfaceType $ foldr (IfaceFunTy VisArg) pat_ty arg_tys ])
       where
         univ_msg = pprUserIfaceForAll univ_bndrs
         ex_msg   = pprUserIfaceForAll ex_bndrs
@@ -1475,8 +1475,7 @@ freeNamesIfType (IfaceTyConApp tc ts) = freeNamesIfTc tc &&& freeNamesIfAppArgs
 freeNamesIfType (IfaceTupleTy _ _ ts) = freeNamesIfAppArgs ts
 freeNamesIfType (IfaceLitTy _)        = emptyNameSet
 freeNamesIfType (IfaceForAllTy tv t)  = freeNamesIfVarBndr tv &&& freeNamesIfType t
-freeNamesIfType (IfaceFunTy s t)      = freeNamesIfType s &&& freeNamesIfType t
-freeNamesIfType (IfaceDFunTy s t)     = freeNamesIfType s &&& freeNamesIfType t
+freeNamesIfType (IfaceFunTy _ s t)    = freeNamesIfType s &&& freeNamesIfType t
 freeNamesIfType (IfaceCastTy t c)     = freeNamesIfType t &&& freeNamesIfCoercion c
 freeNamesIfType (IfaceCoercionTy c)   = freeNamesIfCoercion c
 
index f4032d2..985a612 100644 (file)
@@ -21,7 +21,7 @@ module IfaceType (
         IfaceTyLit(..), IfaceAppArgs(..),
         IfaceContext, IfaceBndr(..), IfaceOneShot(..), IfaceLamBndr,
         IfaceTvBndr, IfaceIdBndr, IfaceTyConBinder,
-        IfaceForAllBndr, ArgFlag(..), ShowForAllFlag(..),
+        IfaceForAllBndr, ArgFlag(..), AnonArgFlag(..), ShowForAllFlag(..),
         mkIfaceForAllTvBndr,
 
         ifForAllBndrVar, ifForAllBndrName, ifaceBndrName,
@@ -135,8 +135,7 @@ data IfaceType
                              -- See Note [Suppressing invisible arguments] for
                              -- an explanation of why the second field isn't
                              -- IfaceType, analogous to AppTy.
-  | IfaceFunTy     IfaceType IfaceType
-  | IfaceDFunTy    IfaceType IfaceType
+  | IfaceFunTy     AnonArgFlag IfaceType IfaceType
   | IfaceForAllTy  IfaceForAllBndr IfaceType
   | IfaceTyConApp  IfaceTyCon IfaceAppArgs  -- Not necessarily saturated
                                             -- Includes newtypes, synonyms, tuples
@@ -394,7 +393,7 @@ splitIfaceSigmaTy ty
         = case split_foralls ty of { (bndrs, rho) -> (bndr:bndrs, rho) }
     split_foralls rho = ([], rho)
 
-    split_rho (IfaceDFunTy ty1 ty2)
+    split_rho (IfaceFunTy InvisArg ty1 ty2)
         = case split_rho ty2 of { (ps, tau) -> (ty1:ps, tau) }
     split_rho tau = ([], tau)
 
@@ -438,8 +437,7 @@ ifTypeIsVarFree ty = go ty
     go (IfaceTyVar {})         = False
     go (IfaceFreeTyVar {})     = False
     go (IfaceAppTy fun args)   = go fun && go_args args
-    go (IfaceFunTy arg res)    = go arg && go res
-    go (IfaceDFunTy arg res)   = go arg && go res
+    go (IfaceFunTy _ arg res)  = go arg && go res
     go (IfaceForAllTy {})      = False
     go (IfaceTyConApp _ args)  = go_args args
     go (IfaceTupleTy _ _ args) = go_args args
@@ -474,8 +472,7 @@ substIfaceType env ty
     go (IfaceFreeTyVar tv)    = IfaceFreeTyVar tv
     go (IfaceTyVar tv)        = substIfaceTyVar env tv
     go (IfaceAppTy  t ts)     = IfaceAppTy  (go t) (substIfaceAppArgs env ts)
-    go (IfaceFunTy  t1 t2)    = IfaceFunTy  (go t1) (go t2)
-    go (IfaceDFunTy t1 t2)    = IfaceDFunTy (go t1) (go t2)
+    go (IfaceFunTy af t1 t2)  = IfaceFunTy af (go t1) (go t2)
     go ty@(IfaceLitTy {})     = ty
     go (IfaceTyConApp tc tys) = IfaceTyConApp tc (substIfaceAppArgs env tys)
     go (IfaceTupleTy s i tys) = IfaceTupleTy s i (substIfaceAppArgs env tys)
@@ -720,7 +717,9 @@ pprIfaceTyConBinders = sep . map go
     go (Bndr (IfaceTvBndr bndr) vis) =
       -- See Note [Pretty-printing invisible arguments]
       case vis of
-        AnonTCB            -> ppr_bndr True
+        AnonTCB  VisArg    -> ppr_bndr True
+        AnonTCB  InvisArg  -> ppr_bndr True  -- Rare; just promoted GADT data constructors
+                                             -- Should we print them differently?
         NamedTCB Required  -> ppr_bndr True
         NamedTCB Specified -> char '@' <> ppr_bndr True
         NamedTCB Inferred  -> char '@' <> braces (ppr_bndr False)
@@ -768,19 +767,26 @@ pprPrecIfaceType :: PprPrec -> IfaceType -> SDoc
 -- called from other places, besides `:type` and `:info`.
 pprPrecIfaceType prec ty = eliminateRuntimeRep (ppr_ty prec) ty
 
+ppr_sigma :: PprPrec -> IfaceType -> SDoc
+ppr_sigma ctxt_prec ty
+  = maybeParen ctxt_prec funPrec (pprIfaceSigmaType ShowForAllMust ty)
+
 ppr_ty :: PprPrec -> IfaceType -> SDoc
+ppr_ty ctxt_prec ty@(IfaceForAllTy {})        = ppr_sigma ctxt_prec ty
+ppr_ty ctxt_prec ty@(IfaceFunTy InvisArg _ _) = ppr_sigma ctxt_prec ty
+
 ppr_ty _         (IfaceFreeTyVar tyvar) = ppr tyvar  -- This is the main reason for IfaceFreeTyVar!
 ppr_ty _         (IfaceTyVar tyvar)     = ppr tyvar  -- See Note [TcTyVars in IfaceType]
 ppr_ty ctxt_prec (IfaceTyConApp tc tys) = pprTyTcApp ctxt_prec tc tys
 ppr_ty ctxt_prec (IfaceTupleTy i p tys) = pprTuple ctxt_prec i p tys
 ppr_ty _         (IfaceLitTy n)         = pprIfaceTyLit n
         -- Function types
-ppr_ty ctxt_prec (IfaceFunTy ty1 ty2)
+ppr_ty ctxt_prec (IfaceFunTy _ ty1 ty2)  -- Should be VisArg
   = -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
     maybeParen ctxt_prec funPrec $
     sep [ppr_ty funPrec ty1, sep (ppr_fun_tail ty2)]
   where
-    ppr_fun_tail (IfaceFunTy ty1 ty2)
+    ppr_fun_tail (IfaceFunTy VisArg ty1 ty2)
       = (arrow <+> ppr_ty funPrec ty1) : ppr_fun_tail ty2
     ppr_fun_tail other_ty
       = [arrow <+> pprIfaceType other_ty]
@@ -819,9 +825,6 @@ ppr_ty ctxt_prec (IfaceCoercionTy co)
       (ppr_co ctxt_prec co)
       (text "<>")
 
-ppr_ty ctxt_prec ty -- IfaceForAllTy
-  = maybeParen ctxt_prec funPrec (pprIfaceSigmaType ShowForAllMust ty)
-
 {- Note [Defaulting RuntimeRep variables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 RuntimeRep variables are considered by many (most?) users to be little
@@ -916,15 +919,12 @@ defaultRuntimeRepVars ty = go False emptyFsEnv ty
     go ink subs (IfaceTupleTy sort is_prom tc_args)
       = IfaceTupleTy sort is_prom (go_args ink subs tc_args)
 
-    go ink subs (IfaceFunTy arg res)
-      = IfaceFunTy (go ink subs arg) (go ink subs res)
+    go ink subs (IfaceFunTy af arg res)
+      = IfaceFunTy af (go ink subs arg) (go ink subs res)
 
     go ink subs (IfaceAppTy t ts)
       = IfaceAppTy (go ink subs t) (go_args ink subs ts)
 
-    go ink subs (IfaceDFunTy x y)
-      = IfaceDFunTy (go ink subs x) (go ink subs y)
-
     go ink subs (IfaceCastTy x co)
       = IfaceCastTy (go ink subs x) co
 
@@ -1673,12 +1673,9 @@ instance Binary IfaceType where
             putByte bh 2
             put_ bh ae
             put_ bh af
-    put_ bh (IfaceFunTy ag ah) = do
+    put_ bh (IfaceFunTy af ag ah) = do
             putByte bh 3
-            put_ bh ag
-            put_ bh ah
-    put_ bh (IfaceDFunTy ag ah) = do
-            putByte bh 4
+            put_ bh af
             put_ bh ag
             put_ bh ah
     put_ bh (IfaceTyConApp tc tys)
@@ -1703,12 +1700,10 @@ instance Binary IfaceType where
               2 -> do ae <- get bh
                       af <- get bh
                       return (IfaceAppTy ae af)
-              3 -> do ag <- get bh
-                      ah <- get bh
-                      return (IfaceFunTy ag ah)
-              4 -> do ag <- get bh
+              3 -> do af <- get bh
+                      ag <- get bh
                       ah <- get bh
-                      return (IfaceDFunTy ag ah)
+                      return (IfaceFunTy af ag ah)
               5 -> do { tc <- get bh; tys <- get bh
                       ; return (IfaceTyConApp tc tys) }
               6 -> do { a <- get bh; b <- get bh
index 29893ca..3874d8d 100644 (file)
@@ -1140,12 +1140,11 @@ tcIfaceCompleteSig (IfaceCompleteMatch ms t) = return (CompleteMatch ms t)
 tcIfaceType :: IfaceType -> IfL Type
 tcIfaceType = go
   where
-    go (IfaceTyVar n)         = TyVarTy <$> tcIfaceTyVar n
-    go (IfaceFreeTyVar n)     = pprPanic "tcIfaceType:IfaceFreeTyVar" (ppr n)
-    go (IfaceLitTy l)         = LitTy <$> tcIfaceTyLit l
-    go (IfaceFunTy t1 t2)     = FunTy <$> go t1 <*> go t2
-    go (IfaceDFunTy t1 t2)    = FunTy <$> go t1 <*> go t2
-    go (IfaceTupleTy s i tks) = tcIfaceTupleTy s i tks
+    go (IfaceTyVar n)          = TyVarTy <$> tcIfaceTyVar n
+    go (IfaceFreeTyVar n)      = pprPanic "tcIfaceType:IfaceFreeTyVar" (ppr n)
+    go (IfaceLitTy l)          = LitTy <$> tcIfaceTyLit l
+    go (IfaceFunTy flag t1 t2) = FunTy flag <$> go t1 <*> go t2
+    go (IfaceTupleTy s i tks)  = tcIfaceTupleTy s i tks
     go (IfaceAppTy t ts)
       = do { t'  <- go t
            ; ts' <- traverse go (appArgsIfaceTypes ts)
index 7c8a939..3779e39 100644 (file)
@@ -140,9 +140,8 @@ toIfaceTypeX fr ty@(AppTy {})  =
 toIfaceTypeX _  (LitTy n)      = IfaceLitTy (toIfaceTyLit n)
 toIfaceTypeX fr (ForAllTy b t) = IfaceForAllTy (toIfaceForAllBndrX fr b)
                                                (toIfaceTypeX (fr `delVarSet` binderVar b) t)
-toIfaceTypeX fr (FunTy t1 t2)
-  | isPredTy t1                 = IfaceDFunTy (toIfaceTypeX fr t1) (toIfaceTypeX fr t2)
-  | otherwise                   = IfaceFunTy  (toIfaceTypeX fr t1) (toIfaceTypeX fr t2)
+toIfaceTypeX fr (FunTy { ft_arg = t1, ft_res = t2, ft_af = af })
+  = IfaceFunTy af (toIfaceTypeX fr t1) (toIfaceTypeX fr t2)
 toIfaceTypeX fr (CastTy ty co)  = IfaceCastTy (toIfaceTypeX fr ty) (toIfaceCoercionX fr co)
 toIfaceTypeX fr (CoercionTy co) = IfaceCoercionTy (toIfaceCoercionX fr co)
 
@@ -310,7 +309,7 @@ toIfaceAppArgsX fr kind ty_args
         t'  = toIfaceTypeX fr t
         ts' = go (extendTCvSubst env tv t) res ts
 
-    go env (FunTy _ res) (t:ts) -- No type-class args in tycon apps
+    go env (FunTy { ft_res = res }) (t:ts) -- No type-class args in tycon apps
       = IA_Arg (toIfaceTypeX fr t) Required (go env res ts)
 
     go env ty ts@(t1:ts1)
index 369f17f..fd1bab3 100644 (file)
@@ -542,7 +542,7 @@ primOpType op
     Compare _occ ty -> compare_fun_ty ty
 
     GenPrimOp _occ tyvars arg_tys res_ty ->
-        mkSpecForAllTys tyvars (mkFunTys arg_tys res_ty)
+        mkSpecForAllTys tyvars (mkVisFunTys arg_tys res_ty)
 
 primOpOcc :: PrimOp -> OccName
 primOpOcc op = case primOpInfo op of
@@ -609,9 +609,9 @@ commutableOp :: PrimOp -> Bool
 -- Utils:
 
 dyadic_fun_ty, monadic_fun_ty, compare_fun_ty :: Type -> Type
-dyadic_fun_ty  ty = mkFunTys [ty, ty] ty
-monadic_fun_ty ty = mkFunTy  ty ty
-compare_fun_ty ty = mkFunTys [ty, ty] intPrimTy
+dyadic_fun_ty  ty = mkVisFunTys [ty, ty] ty
+monadic_fun_ty ty = mkVisFunTy  ty ty
+compare_fun_ty ty = mkVisFunTys [ty, ty] intPrimTy
 
 -- Output stuff:
 
index ddb1211..d3fd0b9 100644 (file)
@@ -106,7 +106,7 @@ import {-# SOURCE #-} TysWiredIn
   , doubleElemRepDataConTy
   , mkPromotedListTy )
 
-import Var              ( TyVar, VarBndr(Bndr), mkTyVar )
+import Var              ( TyVar, mkTyVar )
 import Name
 import TyCon
 import SrcLoc
@@ -320,10 +320,10 @@ mkTemplateKindTyConBinders :: [Kind] -> [TyConBinder]
 mkTemplateKindTyConBinders kinds = [mkNamedTyConBinder Specified tv | tv <- mkTemplateKindVars kinds]
 
 mkTemplateAnonTyConBinders :: [Kind] -> [TyConBinder]
-mkTemplateAnonTyConBinders kinds = map mkAnonTyConBinder (mkTemplateTyVars kinds)
+mkTemplateAnonTyConBinders kinds = mkAnonTyConBinders VisArg (mkTemplateTyVars kinds)
 
 mkTemplateAnonTyConBindersFrom :: Int -> [Kind] -> [TyConBinder]
-mkTemplateAnonTyConBindersFrom n kinds = map mkAnonTyConBinder (mkTemplateTyVarsFrom n kinds)
+mkTemplateAnonTyConBindersFrom n kinds = mkAnonTyConBinders VisArg (mkTemplateTyVarsFrom n kinds)
 
 alphaTyVars :: [TyVar]
 alphaTyVars = mkTemplateTyVars $ repeat liftedTypeKind
@@ -383,9 +383,8 @@ funTyConName = mkPrimTyConName (fsLit "->") funTyConKey funTyCon
 funTyCon :: TyCon
 funTyCon = mkFunTyCon funTyConName tc_bndrs tc_rep_nm
   where
-    tc_bndrs = [ Bndr runtimeRep1TyVar (NamedTCB Inferred)
-               , Bndr runtimeRep2TyVar (NamedTCB Inferred)
-               ]
+    tc_bndrs = [ mkNamedTyConBinder Inferred runtimeRep1TyVar
+               , mkNamedTyConBinder Inferred runtimeRep2TyVar ]
                ++ mkTemplateAnonTyConBinders [ tYPE runtimeRep1Ty
                                              , tYPE runtimeRep2Ty
                                              ]
@@ -680,7 +679,7 @@ Let's take these one at a time:
     --------------------------
 This is The Type Of Equality in GHC. It classifies nominal coercions.
 This type is used in the solver for recording equality constraints.
-It responds "yes" to Type.isEqPred and classifies as an EqPred in
+It responds "yes" to Type.isEqPrimPred and classifies as an EqPred in
 Type.classifyPredType.
 
 All wanted constraints of this type are built with coercion holes.
index 5ea1fd0..4e7cd84 100644 (file)
@@ -16,8 +16,6 @@ module TysWiredIn (
 
         mkWiredInIdName,    -- used in MkId
 
-        mkFunKind, mkForAllKind,
-
         -- * All wired in things
         wiredInTyCons, isBuiltInOcc_maybe,
 
@@ -86,6 +84,9 @@ module TysWiredIn (
         -- * Any
         anyTyCon, anyTy, anyTypeOfKind,
 
+        -- * Recovery TyCon
+        makeRecoveryTyCon,
+
         -- * Sums
         mkSumTy, sumTyCon, sumDataCon,
 
@@ -153,6 +154,7 @@ import NameSet          ( NameSet, mkNameSet, elemNameSet )
 import BasicTypes       ( Arity, Boxity(..), TupleSort(..), ConTagZ,
                           SourceText(..) )
 import ForeignCall
+import Var              ( AnonArgFlag(..) )
 import SrcLoc           ( noSrcSpan )
 import Unique
 import Data.Array
@@ -395,6 +397,29 @@ anyTy = mkTyConTy anyTyCon
 anyTypeOfKind :: Kind -> Type
 anyTypeOfKind kind = mkTyConApp anyTyCon [kind]
 
+-- | Make a fake, recovery 'TyCon' from an existing one.
+-- Used when recovering from errors in type declarations
+makeRecoveryTyCon :: TyCon -> TyCon
+makeRecoveryTyCon tc
+  = mkTcTyCon (tyConName tc)
+              bndrs res_kind
+              []               -- No scoped vars
+              True             -- Fully generalised
+              flavour          -- Keep old flavour
+  where
+    flavour = tyConFlavour tc
+    [kv] = mkTemplateKindVars [liftedTypeKind]
+    (bndrs, res_kind)
+       = case flavour of
+           PromotedDataConFlavour -> ([mkNamedTyConBinder Inferred kv], mkTyVarTy kv)
+           _ -> (tyConBinders tc, tyConResKind tc)
+        -- For data types we have already validated their kind, so it
+        -- makes sense to keep it. For promoted data constructors we haven't,
+        -- so we recover with kind (forall k. k).  Otherwise consider
+        --     data T a where { MkT :: Show a => T a }
+        -- If T is for some reason invalid, we don't want to fall over
+        -- at (promoted) use-sites of MkT.
+
 -- Kinds
 typeNatKindConName, typeSymbolKindConName :: Name
 typeNatKindConName    = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Nat")    typeNatKindConNameKey    typeNatKindCon
@@ -484,7 +509,7 @@ consDataCon_RDR = nameRdrName consDataConName
 pcTyCon :: Name -> Maybe CType -> [TyVar] -> [DataCon] -> TyCon
 pcTyCon name cType tyvars cons
   = mkAlgTyCon name
-                (mkAnonTyConBinders tyvars)
+                (mkAnonTyConBinders VisArg tyvars)
                 liftedTypeKind
                 (map (const Representational) tyvars)
                 cType
@@ -595,14 +620,6 @@ liftedTypeKind, constraintKind :: Kind
 liftedTypeKind   = tYPE liftedRepTy
 constraintKind   = mkTyConApp constraintKindTyCon []
 
--- mkFunKind and mkForAllKind are defined here
--- solely so that TyCon can use them via a SOURCE import
-mkFunKind :: Kind -> Kind -> Kind
-mkFunKind = mkFunTy
-
-mkForAllKind :: TyCoVar -> ArgFlag -> Kind -> Kind
-mkForAllKind = mkForAllTy
-
 {-
 ************************************************************************
 *                                                                      *
index 1481a75..4e8ebba 100644 (file)
@@ -1,13 +1,8 @@
 module TysWiredIn where
 
-import Var( TyVar, ArgFlag )
 import {-# SOURCE #-} TyCon      ( TyCon )
 import {-# SOURCE #-} TyCoRep    (Type, Kind)
 
-
-mkFunKind :: Kind -> Kind -> Kind
-mkForAllKind :: TyVar -> ArgFlag -> Kind -> Kind
-
 listTyCon :: TyCon
 typeNatKind, typeSymbolKind :: Type
 mkBoxedTupleTy :: [Type] -> Type
index 4c59bba..265b0fb 100644 (file)
@@ -412,8 +412,8 @@ contHoleType (StrictBind { sc_bndr = b, sc_dup = dup, sc_env = se })
 contHoleType (StrictArg { sc_fun = ai })      = funArgTy (ai_type ai)
 contHoleType (ApplyToTy  { sc_hole_ty = ty }) = ty  -- See Note [The hole type in ApplyToTy]
 contHoleType (ApplyToVal { sc_arg = e, sc_env = se, sc_dup = dup, sc_cont = k })
-  = mkFunTy (perhapsSubstTy dup se (exprType e))
-            (contHoleType k)
+  = mkVisFunTy (perhapsSubstTy dup se (exprType e))
+               (contHoleType k)
 contHoleType (Select { sc_dup = d, sc_bndr =  b, sc_env = se })
   = perhapsSubstTy d se (idType b)
 
index 4d437d3..d93d716 100644 (file)
@@ -108,7 +108,7 @@ countFunRepArgs :: Arity -> Type -> RepArity
 countFunRepArgs 0 _
   = 0
 countFunRepArgs n ty
-  | FunTy arg res <- unwrapType ty
+  | FunTy arg res <- unwrapType ty
   = length (typePrimRepArgs arg) + countFunRepArgs (n - 1) res
   | otherwise
   = pprPanic "countFunRepArgs: arity greater than type can handle" (ppr (n, ty, typePrimRep ty))
@@ -120,7 +120,7 @@ countConRepArgs dc = go (dataConRepArity dc) (dataConRepType dc)
     go 0 _
       = 0
     go n ty
-      | FunTy arg res <- unwrapType ty
+      | FunTy arg res <- unwrapType ty
       = length (typePrimRep arg) + go (n - 1) res
       | otherwise
       = pprPanic "countConRepArgs: arity greater than type can handle" (ppr (n, ty, typePrimRep ty))
index 516b898..9f58a03 100644 (file)
@@ -670,7 +670,7 @@ matchHasField dflags short_cut clas tys
                          -- the HasField x r a dictionary.  The preds will
                          -- typically be empty, but if the datatype has a
                          -- "stupid theta" then we have to include it here.
-                   ; let theta = mkPrimEqPred sel_ty (mkFunTy r_ty a_ty) : preds
+                   ; let theta = mkPrimEqPred sel_ty (mkVisFunTy r_ty a_ty) : preds
 
                          -- Use the equality proof to cast the selector Id to
                          -- type (r -> a), then use the newtype coercion to cast
index 7efcb97..3f119ea 100644 (file)
@@ -820,7 +820,7 @@ injTyVarsOfType (TyConApp tc tys)
   = injTyVarsOfTypes tys
 injTyVarsOfType (LitTy {})
   = emptyVarSet
-injTyVarsOfType (FunTy arg res)
+injTyVarsOfType (FunTy arg res)
   = injTyVarsOfType arg `unionVarSet` injTyVarsOfType res
 injTyVarsOfType (AppTy fun arg)
   = injTyVarsOfType fun `unionVarSet` injTyVarsOfType arg
index d4348ec..77e8cdf 100644 (file)
@@ -58,7 +58,7 @@ import MkId( mkDictFunId )
 import CoreSyn( Expr(..) )  -- For the Coercion constructor
 import Id
 import Name
-import Var      ( EvVar, mkTyVar, tyVarName, VarBndr(..) )
+import Var      ( EvVar, tyVarName, VarBndr(..) )
 import DataCon
 import VarEnv
 import PrelNames
@@ -158,7 +158,7 @@ deeplySkolemise ty
                       <.> mkWpEvVarApps ids1
                     , tv_prs1  ++ tvs_prs2
                     , ev_vars1 ++ ev_vars2
-                    , mkFunTys arg_tys' rho ) }
+                    , mkVisFunTys arg_tys' rho ) }
 
       | otherwise
       = return (idHsWrapper, [], [], substTy subst ty)
@@ -197,7 +197,7 @@ top_instantiate inst_all orig ty
        ; (subst, inst_tvs') <- mapAccumLM newMetaTyVarX empty_subst inst_tvs
        ; let inst_theta' = substTheta subst inst_theta
              sigma'      = substTy subst (mkForAllTys leave_bndrs $
-                                          mkFunTys leave_theta rho)
+                                          mkPhiTy leave_theta rho)
              inst_tv_tys' = mkTyVarTys inst_tvs'
 
        ; wrap1 <- instCall orig inst_tv_tys' inst_theta'
@@ -272,7 +272,7 @@ deeply_instantiate orig subst ty
                     <.> wrap2
                     <.> wrap1
                     <.> mkWpEvVarApps ids1,
-                 mkFunTys arg_tys' rho2) }
+                 mkVisFunTys arg_tys' rho2) }
 
   | otherwise
   = do { let ty' = substTy subst ty
@@ -402,88 +402,13 @@ instStupidTheta orig theta
   = do  { _co <- instCallConstraints orig theta -- Discard the coercion
         ; return () }
 
-{-
-************************************************************************
+
+{- *********************************************************************
 *                                                                      *
          Instantiating Kinds
 *                                                                      *
-************************************************************************
-
-Note [Constraints handled in types]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Generally, we cannot handle constraints written in types. For example,
-if we declare
-
-  data C a where
-    MkC :: Show a => a -> C a
-
-we will not be able to use MkC in types, as we have no way of creating
-a type-level Show dictionary.
-
-However, we make an exception for equality types. Consider
-
-  data T1 a where
-    MkT1 :: T1 Bool
-
-  data T2 a where
-    MkT2 :: a ~ Bool => T2 a
-
-MkT1 has a constrained return type, while MkT2 uses an explicit equality
-constraint. These two types are often written interchangeably, with a
-reasonable expectation that they mean the same thing. For this to work --
-and for us to be able to promote GADTs -- we need to be able to instantiate
-equality constraints in types.
-
-One wrinkle is that the equality in MkT2 is *lifted*. But, for proper
-GADT equalities, GHC produces *unlifted* constraints. (This unlifting comes
-from DataCon.eqSpecPreds, which uses mkPrimEqPred.) And, perhaps a wily
-user will use (~~) for a heterogeneous equality. We thus must support
-all of (~), (~~), and (~#) in types. (See Note [The equality types story]
-in TysPrim for a primer on these equality types.)
-
-The get_eq_tys_maybe function recognizes these three forms of equality,
-returning a suitable type formation function and the two types related
-by the equality constraint. In the lifted case, it uses mkHEqBoxTy or
-mkEqBoxTy, which promote the datacons of the (~~) or (~) datatype,
-respectively.
-
-One might reasonably wonder who *unpacks* these boxes once they are
-made. After all, there is no type-level `case` construct. The surprising
-answer is that no one ever does. Instead, if a GADT constructor is used
-on the left-hand side of a type family equation, that occurrence forces
-GHC to unify the types in question. For example:
-
-  data G a where
-    MkG :: G Bool
-
-  type family F (x :: G a) :: a where
-    F MkG = False
-
-When checking the LHS `F MkG`, GHC sees the MkG constructor and then must
-unify F's implicit parameter `a` with Bool. This succeeds, making the equation
+********************************************************************* -}
 
-    F Bool (MkG @Bool <Bool>) = False
-
-Note that we never need unpack the coercion. This is because type family
-equations are *not* parametric in their kind variables. That is, we could have
-just said
-
-  type family H (x :: G a) :: a where
-    H _ = False
-
-The presence of False on the RHS also forces `a` to become Bool, giving us
-
-    H Bool _ = False
-
-The fact that any of this works stems from the lack of phase separation between
-types and kinds (unlike the very present phase separation between terms and types).
-
-Once we have the ability to pattern-match on types below top-level, this will
-no longer cut it, but it seems fine for now.
-
--}
-
----------------------------
 -- | Instantiates up to n invisible binders
 -- Returns the instantiating types, and body kind
 tcInstInvisibleTyBinders :: Int -> TcKind -> TcM ([TcType], TcKind)
@@ -511,61 +436,42 @@ tcInstInvisibleTyBinder subst (Named (Bndr tv _))
   = do { (subst', tv') <- newMetaTyVarX subst tv
        ; return (subst', mkTyVarTy tv') }
 
-tcInstInvisibleTyBinder subst (Anon ty)
-     -- This is the *only* constraint currently handled in types.
-  | Just (mk, k1, k2) <- get_eq_tys_maybe substed_ty
-  = do { co <- unifyKind Nothing k1 k2
+tcInstInvisibleTyBinder subst (Anon af ty)
+  | Just (mk, k1, k2) <- get_eq_tys_maybe (substTy subst ty)
+    -- Equality is the *only* constraint currently handled in types.
+    -- See Note [Constraints in kinds] in TyCoRep
+  = ASSERT( af == InvisArg )
+    do { co <- unifyKind Nothing k1 k2
        ; arg' <- mk co
        ; return (subst, arg') }
 
-  | isPredTy substed_ty
-  = do { let (env, tidy_ty) = tidyOpenType emptyTidyEnv substed_ty
-       ; addErrTcM (env, text "Illegal constraint in a kind:" <+> ppr tidy_ty)
-
-         -- just invent a new variable so that we can continue
-       ; u <- newUnique
-       ; let name = mkSysTvName u (fsLit "dict")
-       ; return (subst, mkTyVarTy $ mkTyVar name substed_ty) }
+  | otherwise  -- This should never happen
+               -- See TyCoRep Note [Constraints in kinds]
+  = pprPanic "tcInvisibleTyBinder" (ppr ty)
 
+-------------------------------
+get_eq_tys_maybe :: Type
+                 -> Maybe ( Coercion -> TcM Type
+                             -- given a coercion proving t1 ~# t2, produce the
+                             -- right instantiation for the TyBinder at hand
+                          , Type  -- t1
+                          , Type  -- t2
+                          )
+-- See Note [Constraints in kinds] in TyCoRep
+get_eq_tys_maybe ty
+  -- Lifted heterogeneous equality (~~)
+  | Just (tc, [_, _, k1, k2]) <- splitTyConApp_maybe ty
+  , tc `hasKey` heqTyConKey
+  = Just (\co -> mkHEqBoxTy co k1 k2, k1, k2)
+
+  -- Lifted homogeneous equality (~)
+  | Just (tc, [_, k1, k2]) <- splitTyConApp_maybe ty
+  , tc `hasKey` eqTyConKey
+  = Just (\co -> mkEqBoxTy co k1 k2, k1, k2)
 
   | otherwise
-  = do { tv_ty <- newFlexiTyVarTy substed_ty
-       ; return (subst, tv_ty) }
-
-  where
-    substed_ty = substTy subst ty
-
-      -- See Note [Constraints handled in types]
-    get_eq_tys_maybe :: Type
-                     -> Maybe ( Coercion -> TcM Type
-                                 -- given a coercion proving t1 ~# t2, produce the
-                                 -- right instantiation for the TyBinder at hand
-                              , Type  -- t1
-                              , Type  -- t2
-                              )
-    get_eq_tys_maybe ty
-        -- unlifted equality (~#)
-      | Just (Nominal, k1, k2) <- getEqPredTys_maybe ty
-      = Just (\co -> return $ mkCoercionTy co, k1, k2)
-
-        -- lifted heterogeneous equality (~~)
-      | Just (tc, [_, _, k1, k2]) <- splitTyConApp_maybe ty
-      = if | tc `hasKey` heqTyConKey
-             -> Just (\co -> mkHEqBoxTy co k1 k2, k1, k2)
-           | otherwise
-             -> Nothing
-
-        -- lifted homogeneous equality (~)
-      | Just (tc, [_, k1, k2]) <- splitTyConApp_maybe ty
-      = if | tc `hasKey` eqTyConKey
-             -> Just (\co -> mkEqBoxTy co k1 k2, k1, k2)
-           | otherwise
-             -> Nothing
-
-      | otherwise
-      = Nothing
+  = Nothing
 
--------------------------------
 -- | This takes @a ~# b@ and returns @a ~~ b@.
 mkHEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
 -- monadic just for convenience with mkEqBoxTy
index 96adf46..763684b 100644 (file)
@@ -308,7 +308,7 @@ tc_cmd env cmd@(HsCmdArrForm x expr f fixity cmd_args) (cmd_stk, res_ty)
     do  { (cmd_args', cmd_tys) <- mapAndUnzipM tc_cmd_arg cmd_args
                               -- We use alphaTyVar for 'w'
         ; let e_ty = mkInvForAllTy alphaTyVar $
-                     mkFunTys cmd_tys $
+                     mkVisFunTys cmd_tys $
                      mkCmdArrTy env (mkPairTy alphaTy cmd_stk) res_ty
         ; expr' <- tcPolyExpr expr e_ty
         ; return (HsCmdArrForm x expr' f fixity cmd_args') }
@@ -426,7 +426,7 @@ mkPairTy :: Type -> Type -> Type
 mkPairTy t1 t2 = mkTyConApp pairTyCon [t1,t2]
 
 arrowTyConKind :: Kind          --  *->*->*
-arrowTyConKind = mkFunTys [liftedTypeKind, liftedTypeKind] liftedTypeKind
+arrowTyConKind = mkVisFunTys [liftedTypeKind, liftedTypeKind] liftedTypeKind
 
 {-
 ************************************************************************
index 09ef93a..9abc048 100644 (file)
@@ -824,7 +824,6 @@ is flattened, but this is left as future work. (Mar '15)
 
 Note [FunTy and decomposing tycon applications]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
 When can_eq_nc' attempts to decompose a tycon application we haven't yet zonked.
 This means that we may very well have a FunTy containing a type of some unknown
 kind. For instance, we may have,
@@ -923,8 +922,8 @@ can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
 -- Including FunTy (s -> t)
 can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1 _ ty2 _
     --- See Note [FunTy and decomposing type constructor applications].
-  | Just (tc1, tys1) <- tcRepSplitTyConApp_maybe' ty1
-  , Just (tc2, tys2) <- tcRepSplitTyConApp_maybe' ty2
+  | Just (tc1, tys1) <- repSplitTyConApp_maybe ty1
+  , Just (tc2, tys2) <- repSplitTyConApp_maybe ty2
   , not (isTypeFamilyTyCon tc1)
   , not (isTypeFamilyTyCon tc2)
   = canTyConApp ev eq_rel tc1 tys1 tc2 tys2
@@ -1080,7 +1079,7 @@ zonk_eq_types = go
       , Just (arg2, res2) <- split2
       = do { res_a <- go arg1 arg2
            ; res_b <- go res1 res2
-           ; return $ combine_rev mkFunTy res_b res_a
+           ; return $ combine_rev mkVisFunTy res_b res_a
            }
       | isJust split1 || isJust split2
       = bale_out ty1 ty2
@@ -1089,8 +1088,8 @@ zonk_eq_types = go
         split2 = tcSplitFunTy_maybe ty2
 
     go ty1 ty2
-      | Just (tc1, tys1) <- tcRepSplitTyConApp_maybe ty1
-      , Just (tc2, tys2) <- tcRepSplitTyConApp_maybe ty2
+      | Just (tc1, tys1) <- repSplitTyConApp_maybe ty1
+      , Just (tc2, tys2) <- repSplitTyConApp_maybe ty2
       = if tc1 == tc2 && tys1 `equalLength` tys2
           -- Crucial to check for equal-length args, because
           -- we cannot assume that the two args to 'go' have
@@ -2386,7 +2385,7 @@ unifyWanted loc role orig_ty1 orig_ty2
     go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
     go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
 
-    go (FunTy s1 t1) (FunTy s2 t2)
+    go (FunTy _ s1 t1) (FunTy _ s2 t2)
       = do { co_s <- unifyWanted loc role s1 s2
            ; co_t <- unifyWanted loc role t1 t2
            ; return (mkFunCo role co_s co_t) }
@@ -2437,7 +2436,7 @@ unify_derived loc role    orig_ty1 orig_ty2
     go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
     go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
 
-    go (FunTy s1 t1) (FunTy s2 t2)
+    go (FunTy _ s1 t1) (FunTy _ s2 t2)
       = do { unify_derived loc role s1 s2
            ; unify_derived loc role t1 t2 }
     go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
index ba45e09..d38c922 100644 (file)
@@ -281,7 +281,7 @@ inferConstraintsDataConArgs inst_ty inst_tys
                             , tvs', inst_tys') }
 
 typeToTypeKind :: Kind
-typeToTypeKind = liftedTypeKind `mkFunTy` liftedTypeKind
+typeToTypeKind = liftedTypeKind `mkVisFunTy` liftedTypeKind
 
 -- | Like 'inferConstraints', but used only in the case of @DeriveAnyClass@,
 -- which gathers its constraints based on the type signatures of the class's
index ab48326..d56e344 100644 (file)
@@ -2199,10 +2199,11 @@ expandSynonymsToMatch ty1 ty2 = (ty1_ret, ty2_ret)
           (t1_2', t2_2') = go t1_2 t2_2
        in (mkAppTy t1_1' t1_2', mkAppTy t2_1' t2_2')
 
-    go (FunTy t1_1 t1_2) (FunTy t2_1 t2_2) =
+    go ty1@(FunTy _ t1_1 t1_2) ty2@(FunTy _ t2_1 t2_2) =
       let (t1_1', t2_1') = go t1_1 t2_1
           (t1_2', t2_2') = go t1_2 t2_2
-       in (mkFunTy t1_1' t1_2', mkFunTy t2_1' t2_2')
+       in ( ty1 { ft_arg = t1_1', ft_res = t1_2' }
+          , ty2 { ft_arg = t2_1', ft_res = t2_2' })
 
     go (ForAllTy b1 t1) (ForAllTy b2 t2) =
       -- NOTE: We may have a bug here, but we just can't reproduce it easily.
index 1d6098d..9ee23eb 100644 (file)
@@ -305,7 +305,7 @@ mkWpFuns args res_ty res_wrap doc = snd $ go args res_ty res_wrap
     go [] res_ty res_wrap = (res_ty, res_wrap)
     go ((arg_ty, arg_wrap) : args) res_ty res_wrap
       = let (tail_ty, tail_wrap) = go args res_ty res_wrap in
-        (arg_ty `mkFunTy` tail_ty, mkWpFun arg_wrap tail_wrap arg_ty tail_ty doc)
+        (arg_ty `mkVisFunTy` tail_ty, mkWpFun arg_wrap tail_wrap arg_ty tail_ty doc)
 
 mkWpCastR :: TcCoercionR -> HsWrapper
 mkWpCastR co
index b87f877..d8c53aa 100644 (file)
@@ -439,7 +439,7 @@ tcExpr expr@(SectionR x op arg2) res_ty
        ; (wrap_fun, [arg1_ty, arg2_ty], op_res_ty)
                   <- matchActualFunTys (mk_op_msg op) fn_orig (Just (unLoc op)) 2 op_ty
        ; wrap_res <- tcSubTypeHR SectionOrigin (Just expr)
-                                 (mkFunTy arg1_ty op_res_ty) res_ty
+                                 (mkVisFunTy arg1_ty op_res_ty) res_ty
        ; arg2' <- tcArg op arg2 arg2_ty 2
        ; return ( mkHsWrap wrap_res $
                   SectionR x (mkLHsWrap wrap_fun op') arg2' ) }
@@ -459,7 +459,7 @@ tcExpr expr@(SectionL x arg1 op) res_ty
            <- matchActualFunTys (mk_op_msg op) fn_orig (Just (unLoc op))
                                 n_reqd_args op_ty
        ; wrap_res <- tcSubTypeHR SectionOrigin (Just expr)
-                                 (mkFunTys arg_tys op_res_ty) res_ty
+                                 (mkVisFunTys arg_tys op_res_ty) res_ty
        ; arg1' <- tcArg op arg1 arg1_ty 1
        ; return ( mkHsWrap wrap_res $
                   SectionL x arg1' (mkLHsWrap wrap_fn op') ) }
@@ -491,7 +491,7 @@ tcExpr expr@(ExplicitTuple x tup_args boxity) res_ty
            { Boxed   -> newFlexiTyVarTys arity liftedTypeKind
            ; Unboxed -> replicateM arity newOpenFlexiTyVarTy }
        ; let actual_res_ty
-                 = mkFunTys [ty | (ty, (L _ (Missing _))) <- arg_tys `zip` tup_args]
+                 = mkVisFunTys [ty | (ty, (L _ (Missing _))) <- arg_tys `zip` tup_args]
                             (mkTupleTy boxity arg_tys)
 
        ; wrap <- tcSubTypeHR (Shouldn'tHappenOrigin "ExpTuple")
@@ -1169,7 +1169,7 @@ tcApp m_herald fun@(L loc (HsVar _ (L _ fun_id))) args res_ty
   = do { rep <- newFlexiTyVarTy runtimeRepTy
        ; let [alpha, beta] = mkTemplateTyVars [liftedTypeKind, tYPE rep]
              seq_ty = mkSpecForAllTys [alpha,beta]
-                      (mkTyVarTy alpha `mkFunTy` mkTyVarTy beta `mkFunTy` mkTyVarTy beta)
+                      (mkTyVarTy alpha `mkVisFunTy` mkTyVarTy beta `mkVisFunTy` mkTyVarTy beta)
              seq_fun = L loc (HsVar noExt (L loc seqId))
              -- seq_ty = forall (a:*) (b:TYPE r). a -> b -> b
              -- where 'r' is a meta type variable
@@ -1451,9 +1451,11 @@ tcSyntaxOpGen :: CtOrigin
               -> TcM (a, SyntaxExpr GhcTcId)
 tcSyntaxOpGen orig op arg_tys res_ty thing_inside
   = do { (expr, sigma) <- tcInferSigma $ noLoc $ syn_expr op
+       ; traceTc "tcSyntaxOpGen" (ppr op $$ ppr expr $$ ppr sigma)
        ; (result, expr_wrap, arg_wraps, res_wrap)
            <- tcSynArgA orig sigma arg_tys res_ty $
               thing_inside
+       ; traceTc "tcSyntaxOpGen" (ppr op $$ ppr expr $$ ppr sigma )
        ; return (result, SyntaxExpr { syn_expr = mkHsWrap expr_wrap $ unLoc expr
                                     , syn_arg_wraps = arg_wraps
                                     , syn_res_wrap  = res_wrap }) }
index aa2c020..80202b7 100644 (file)
@@ -1114,11 +1114,12 @@ flatten_one (TyConApp tc tys)
 --                   _ -> fmode
   = flatten_ty_con_app tc tys
 
-flatten_one (FunTy ty1 ty2)
+flatten_one ty@(FunTy _ ty1 ty2)
   = do { (xi1,co1) <- flatten_one ty1
        ; (xi2,co2) <- flatten_one ty2
        ; role <- getRole
-       ; return (mkFunTy xi1 xi2, mkFunCo role co1 co2) }
+       ; return (ty { ft_arg = xi1, ft_res = xi2 }
+                , mkFunCo role co1 co2) }
 
 flatten_one ty@(ForAllTy {})
 -- TODO (RAE): This is inadequate, as it doesn't flatten the kind of
@@ -1859,8 +1860,9 @@ split_pi_tys' ty = split ty ty
   split orig_ty ty | Just ty' <- coreView ty = split orig_ty ty'
   split _       (ForAllTy b res) = let (bs, ty, _) = split res res
                                    in  (Named b : bs, ty, True)
-  split _       (FunTy arg res)  = let (bs, ty, named) = split res res
-                                   in  (Anon arg : bs, ty, named)
+  split _       (FunTy { ft_af = af, ft_arg = arg, ft_res = res })
+                                 = let (bs, ty, named) = split res res
+                                   in  (Anon af arg : bs, ty, named)
   split orig_ty _                = ([], orig_ty, False)
 {-# INLINE split_pi_tys' #-}
 
@@ -1871,7 +1873,7 @@ ty_con_binders_ty_binders' = foldr go ([], False)
   where
     go (Bndr tv (NamedTCB vis)) (bndrs, _)
       = (Named (Bndr tv vis) : bndrs, True)
-    go (Bndr tv AnonTCB)        (bndrs, n)
-      = (Anon (tyVarKind tv)   : bndrs, n)
+    go (Bndr tv (AnonTCB af))   (bndrs, n)
+      = (Anon af (tyVarKind tv)   : bndrs, n)
     {-# INLINE go #-}
 {-# INLINE ty_con_binders_ty_binders' #-}
index 8038de3..4e5feb4 100644 (file)
@@ -277,7 +277,7 @@ tcCheckFIType arg_tys res_ty (CImport (L lc cconv) safety mh l@(CLabel _) src)
   = do checkCg checkCOrAsmOrLlvmOrInterp
        -- NB check res_ty not sig_ty!
        --    In case sig_ty is (forall a. ForeignPtr a)
-       check (isFFILabelTy (mkFunTys arg_tys res_ty)) (illegalForeignTyErr Outputable.empty)
+       check (isFFILabelTy (mkVisFunTys arg_tys res_ty)) (illegalForeignTyErr Outputable.empty)
        cconv' <- checkCConv cconv
        return (CImport (L lc cconv') safety mh l src)
 
@@ -307,7 +307,7 @@ tcCheckFIType arg_tys res_ty idecl@(CImport (L lc cconv) (L ls safety) mh
           addErrTc (illegalForeignTyErr Outputable.empty (text "At least one argument expected"))
         (arg1_ty:arg_tys) -> do
           dflags <- getDynFlags
-          let curried_res_ty = mkFunTys arg_tys res_ty
+          let curried_res_ty = mkVisFunTys arg_tys res_ty
           check (isFFIDynTy curried_res_ty arg1_ty)
                 (illegalForeignTyErr argument)
           checkForeignArgs (isFFIArgumentTy dflags safety) arg_tys
index 701df5f..e4f50dd 100644 (file)
@@ -1443,8 +1443,8 @@ gen_data dflags data_type_name constr_names loc rep_tc
 
 
 kind1, kind2 :: Kind
-kind1 = liftedTypeKind `mkFunTy` liftedTypeKind
-kind2 = liftedTypeKind `mkFunTy` kind1
+kind1 = liftedTypeKind `mkVisFunTy` liftedTypeKind
+kind2 = liftedTypeKind `mkVisFunTy` kind1
 
 gfoldl_RDR, gunfold_RDR, toConstr_RDR, dataTypeOf_RDR, mkConstr_RDR,
     mkDataType_RDR, conIndex_RDR, prefix_RDR, infix_RDR,
@@ -1956,7 +1956,7 @@ genAuxBindSpec dflags loc (DerivCon2Tag tycon)
 
     sig_ty = mkLHsSigWcType $ L loc $ XHsType $ NHsCoreTy $
              mkSpecSigmaTy (tyConTyVars tycon) (tyConStupidTheta tycon) $
-             mkParentType tycon `mkFunTy` intPrimTy
+             mkParentType tycon `mkVisFunTy` intPrimTy
 
     lots_of_constructors = tyConFamilySize tycon > 8
                         -- was: mAX_FAMILY_SIZE_FOR_VEC_RETURNS
@@ -1980,7 +1980,7 @@ genAuxBindSpec dflags loc (DerivTag2Con tycon)
   where
     sig_ty = mkLHsSigWcType $ L loc $
              XHsType $ NHsCoreTy $ mkSpecForAllTys (tyConTyVars tycon) $
-             intTy `mkFunTy` mkParentType tycon
+             intTy `mkVisFunTy` mkParentType tycon
 
     rdr_name = tag2con_RDR dflags tycon
 
index 41d8eb8..02f45ad 100644 (file)
@@ -369,10 +369,11 @@ functorLikeTraverse var (FT { ft_triv = caseTrivial,     ft_var = caseVar
 
     go co ty | Just ty' <- tcView ty = go co ty'
     go co (TyVarTy    v) | v == var = (if co then caseCoVar else caseVar,True)
-    go co (FunTy x y)  | isPredTy x = go co y
-                       | xc || yc   = (caseFun xr yr,True)
-        where (xr,xc) = go (not co) x
-              (yr,yc) = go co       y
+    go co (FunTy { ft_arg = x, ft_res = y, ft_af = af })
+       | InvisArg <- af = go co y
+       | xc || yc       = (caseFun xr yr,True)
+       where (xr,xc) = go (not co) x
+             (yr,yc) = go co       y
     go co (AppTy    x y) | xc = (caseWrongArg,   True)
                          | yc = (caseTyApp x yr, True)
         where (_, xc) = go co x
index 843ec84..3f2556c 100644 (file)
@@ -676,7 +676,7 @@ findValidHoleFits tidy_env implics simples ct | isExprHoleCt ct =
       where newTyVars = replicateM refLvl $ setLvl <$>
                             (newOpenTypeKind >>= newFlexiTyVar)
             setLvl = flip setMetaTyVarTcLevel hole_lvl
-            wrapWithVars vars = mkFunTys (map mkTyVarTy vars) hole_ty
+            wrapWithVars vars = mkVisFunTys (map mkTyVarTy vars) hole_ty
 
     sortFits :: SortingAlg    -- How we should sort the hole fits
              -> [HoleFit]     -- The subs to sort
index c40d8b5..467c604 100644 (file)
@@ -80,7 +80,7 @@ import TyCoRep  ( Type(..) )
 import TcErrors ( reportAllUnsolved )
 import TcType
 import Inst   ( tcInstInvisibleTyBinders, tcInstInvisibleTyBinder )
-import TyCoRep( TyCoBinder(..), tyCoBinderArgFlag )  -- Used in etaExpandAlgTyCon
+import TyCoRep( TyCoBinder(..) )  -- Used in etaExpandAlgTyCon
 import Type
 import TysPrim
 import Coercion
@@ -622,7 +622,6 @@ tc_lhs_type mode (L span ty) exp_kind
   = setSrcSpan span $
     tc_hs_type mode ty exp_kind
 
-------------------------------------------
 tc_hs_type :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
 -- See Note [Bidirectional type checking]
 
@@ -822,12 +821,12 @@ tc_fun_type mode ty1 ty2 exp_kind = case mode_level mode of
        ; res_k <- newOpenTypeKind
        ; ty1' <- tc_lhs_type mode ty1 arg_k
        ; ty2' <- tc_lhs_type mode ty2 res_k
-       ; checkExpectedKind (HsFunTy noExt ty1 ty2) (mkFunTy ty1' ty2')
+       ; checkExpectedKind (HsFunTy noExt ty1 ty2) (mkVisFunTy ty1' ty2')
                            liftedTypeKind exp_kind }
   KindLevel ->  -- no representation polymorphism in kinds. yet.
     do { ty1' <- tc_lhs_type mode ty1 liftedTypeKind
        ; ty2' <- tc_lhs_type mode ty2 liftedTypeKind
-       ; checkExpectedKind (HsFunTy noExt ty1 ty2) (mkFunTy ty1' ty2')
+       ; checkExpectedKind (HsFunTy noExt ty1 ty2) (mkVisFunTy ty1' ty2')
                            liftedTypeKind exp_kind }
 
 ---------------------------
@@ -1047,17 +1046,17 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args
 
       ---------------- HsTypeArg: a kind application (fun @ki)
       (HsTypeArg _ hs_ki_arg : hs_args, Just (ki_binder, inner_ki)) ->
-        case tyCoBinderArgFlag ki_binder of
+        case ki_binder of
 
         -- FunTy with PredTy on LHS, or ForAllTy with Inferred
-        Inferred  -> instantiate ki_binder inner_ki
+        Named (Bndr _ Inferred) -> instantiate ki_binder inner_ki
+        Anon InvisArg _         -> instantiate ki_binder inner_ki
 
-        -- Specified (invisible) binder with visible kind argument
-        Specified ->
+        Named (Bndr _ Specified) ->  -- Visible kind application
           do { traceTc "tcInferApps (vis kind app)"
                        (vcat [ ppr ki_binder, ppr hs_ki_arg
                              , ppr (tyBinderType ki_binder)
-                             , ppr subst, ppr (tyCoBinderArgFlag ki_binder) ])
+                             , ppr subst ])
 
              ; let exp_kind = substTy subst $ tyBinderType ki_binder
 
@@ -1072,17 +1071,10 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args
              ; (subst', fun') <- mkAppTyM subst fun ki_binder ki_arg
              ; go (n+1) fun' subst' inner_ki hs_args }
 
-        -- Visible kind application, but we need a normal type application; error.
-        -- This happens when we have (fun @ki) but (fun :: k1 -> k2),
-        -- that is, without a forall
-        Required ->
-          do { traceTc "tcInferApps (error)"
-                       (vcat [ ppr ki_binder
-                             , ppr hs_ki_arg
-                             , ppr (tyBinderType ki_binder)
-                             , ppr subst
-                             , ppr (isInvisibleBinder ki_binder) ])
-             ; ty_app_err hs_ki_arg $ substTy subst fun_ki }
+        -- Attempted visible kind application (fun @ki), but fun_ki is
+        --   forall k -> blah   or   k1 -> k2
+        -- So we need a normal application.  Error.
+        _ -> ty_app_err hs_ki_arg $ substTy subst fun_ki
 
       -- No binder; try applying the substitution, or fail if that's not possible
       (HsTypeArg _ ki_arg : _, Nothing) -> try_again_after_substing_or $
@@ -1091,7 +1083,7 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args
       ---------------- HsValArg: a nomal argument (fun ty)
       (HsValArg arg : args, Just (ki_binder, inner_ki))
         -- next binder is invisible; need to instantiate it
-        | isInvisibleBinder ki_binder   -- FunTy with PredTy on LHS;
+        | isInvisibleBinder ki_binder   -- FunTy with InvisArg on LHS;
                                         -- or ForAllTy with Inferred or Specified
          -> instantiate ki_binder inner_ki
 
@@ -1129,9 +1121,7 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args
       where
         instantiate ki_binder inner_ki
           = do { traceTc "tcInferApps (need to instantiate)"
-                         (vcat [ ppr ki_binder
-                               , ppr subst
-                               , ppr (tyCoBinderArgFlag ki_binder)])
+                         (vcat [ ppr ki_binder, ppr subst])
                ; (subst', arg') <- tcInstInvisibleTyBinder subst ki_binder
                ; go n (mkAppTy fun arg') subst' inner_ki all_args }
                  -- Because tcInvisibleTyBinder instantiate ki_binder,
@@ -1438,6 +1428,7 @@ tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
                        -- see Trac #15245
                        promotionErr name FamDataConPE
                    ; let (_, _, _, theta, _, _) = dataConFullSig dc
+                   ; traceTc "tcTyVar" (ppr dc <+> ppr theta $$ ppr (dc_theta_illegal_constraint theta))
                    ; case dc_theta_illegal_constraint theta of
                        Just pred -> promotionErr name $
                                     ConstrainedDataConPE pred
@@ -1458,15 +1449,9 @@ tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
 
     -- We cannot promote a data constructor with a context that contains
     -- constraints other than equalities, so error if we find one.
-    -- See Note [Constraints handled in types] in Inst.
+    -- See Note [Constraints in kinds] in TyCoRep
     dc_theta_illegal_constraint :: ThetaType -> Maybe PredType
-    dc_theta_illegal_constraint = find go
-      where
-        go :: PredType -> Bool
-        go pred | Just tc <- tyConAppTyCon_maybe pred
-                = not $  tc `hasKey` eqTyConKey
-                      || tc `hasKey` heqTyConKey
-                | otherwise = True
+    dc_theta_illegal_constraint = find (not . isEqPred)
 
 {-
 Note [GADT kind self-reference]
@@ -1960,7 +1945,7 @@ kcLHsQTyVars_NonCusk name flav
        | hsLTyVarName hs_tv `elemNameSet` dep_names
        = mkNamedTyConBinder Required tv
        | otherwise
-       = mkAnonTyConBinder tv
+       = mkAnonTyConBinder VisArg tv
 
 kcLHsQTyVars_NonCusk _ _ (XLHsQTyVars _) _ = panic "kcLHsQTyVars"
 
@@ -2388,13 +2373,13 @@ etaExpandAlgTyCon tc_bndrs kind
       = case splitPiTy_maybe kind of
           Nothing -> (reverse acc, substTy subst kind)
 
-          Just (Anon arg, kind')
+          Just (Anon arg, kind')
             -> go loc occs' uniqs' subst' (tcb : acc) kind'
             where
               arg'   = substTy subst arg
               tv     = mkTyVar (mkInternalName uniq occ loc) arg'
               subst' = extendTCvInScope subst tv
-              tcb    = Bndr tv AnonTCB
+              tcb    = Bndr tv (AnonTCB VisArg)
               (uniq:uniqs') = uniqs
               (occ:occs')   = occs
 
@@ -2423,7 +2408,7 @@ tcbVisibilities tc orig_args
     go fun_kind subst all_args@(arg : args)
       | Just (tcb, inner_kind) <- splitPiTy_maybe fun_kind
       = case tcb of
-          Anon _              -> AnonTCB      : go inner_kind subst  args
+          Anon af _           -> AnonTCB af   : go inner_kind subst  args
           Named (Bndr tv vis) -> NamedTCB vis : go inner_kind subst' args
                  where
                     subst' = extendTCvSubst subst tv arg
index c1fd0da..7314dd7 100644 (file)
@@ -1219,7 +1219,8 @@ tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds sc_theta
            ; sc_top_name  <- newName (mkSuperDictAuxOcc n (getOccName cls))
            ; sc_ev_id     <- newEvVar sc_pred
            ; addTcEvBind ev_binds_var $ mkWantedEvBind sc_ev_id sc_ev_tm
-           ; let sc_top_ty = mkInvForAllTys tyvars (mkLamTypes dfun_evs sc_pred)
+           ; let sc_top_ty = mkInvForAllTys tyvars $
+                             mkPhiTy (map idType dfun_evs) sc_pred
                  sc_top_id = mkLocalId sc_top_name sc_top_ty
                  export = ABE { abe_ext  = noExt
                               , abe_wrap = idHsWrapper
index ded352c..19fbade 100644 (file)
@@ -172,8 +172,8 @@ newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence
 -- Deals with both equality and non-equality predicates
 newWanted orig t_or_k pty
   = do loc <- getCtLocM orig t_or_k
-       d <- if isEqPred pty then HoleDest  <$> newCoercionHole pty
-                            else EvVarDest <$> newEvVar pty
+       d <- if isEqPrimPred pty then HoleDest  <$> newCoercionHole pty
+                                else EvVarDest <$> newEvVar pty
        return $ CtWanted { ctev_dest = d
                          , ctev_pred = pty
                          , ctev_nosh = WDeriv
@@ -1198,13 +1198,13 @@ collect_cand_qtvs is_dep bound dvs ty
     -----------------
     go :: CandidatesQTvs -> TcType -> TcM CandidatesQTvs
     -- Uses accumulating-parameter style
-    go dv (AppTy t1 t2)    = foldlM go dv [t1, t2]
-    go dv (TyConApp _ tys) = foldlM go dv tys
-    go dv (FunTy arg res)  = foldlM go dv [arg, res]
-    go dv (LitTy {})       = return dv
-    go dv (CastTy ty co)   = do dv1 <- go dv ty
-                                collect_cand_qtvs_co bound dv1 co
-    go dv (CoercionTy co)  = collect_cand_qtvs_co bound dv co
+    go dv (AppTy t1 t2)     = foldlM go dv [t1, t2]
+    go dv (TyConApp _ tys)  = foldlM go dv tys
+    go dv (FunTy _ arg res) = foldlM go dv [arg, res]
+    go dv (LitTy {})        = return dv
+    go dv (CastTy ty co)    = do dv1 <- go dv ty
+                                 collect_cand_qtvs_co bound dv1 co
+    go dv (CoercionTy co)   = collect_cand_qtvs_co bound dv co
 
     go dv (TyVarTy tv)
       | is_bound tv = return dv
@@ -2156,8 +2156,8 @@ tidySigSkol env cx ty tv_prs
       where
         (env', tv') = tidy_tv_bndr env tv
 
-    tidy_ty env (FunTy arg res)
-      = FunTy (tidyType env arg) (tidy_ty env res)
+    tidy_ty env ty@(FunTy _ arg res)
+      = ty { ft_arg = tidyType env arg, ft_res = tidy_ty env res }
 
     tidy_ty env ty = tidyType env ty
 
index 6bc988a..4286a54 100644 (file)
@@ -499,14 +499,14 @@ tcLcStmt m_tc ctxt (TransStmt { trS_form = form, trS_stmts = stmts
              by_arrow :: Type -> Type     -- Wraps 'ty' to '(a->t) -> ty' if the By is present
              by_arrow = case by' of
                           Nothing       -> \ty -> ty
-                          Just (_,e_ty) -> \ty -> (alphaTy `mkFunTy` e_ty) `mkFunTy` ty
+                          Just (_,e_ty) -> \ty -> (alphaTy `mkVisFunTy` e_ty) `mkVisFunTy` ty
 
              tup_ty        = mkBigCoreVarTupTy bndr_ids
              poly_arg_ty   = m_app alphaTy
              poly_res_ty   = m_app (n_app alphaTy)
              using_poly_ty = mkInvForAllTy alphaTyVar $
                              by_arrow $
-                             poly_arg_ty `mkFunTy` poly_res_ty
+                             poly_arg_ty `mkVisFunTy` poly_res_ty
 
        ; using' <- tcPolyExpr using using_poly_ty
        ; let final_using = fmap (mkHsWrap (WpTyApp tup_ty)) using'
@@ -619,7 +619,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap
                          , trS_by = by, trS_using = using, trS_form = form
                          , trS_ret = return_op, trS_bind = bind_op
                          , trS_fmap = fmap_op }) res_ty thing_inside
-  = do { let star_star_kind = liftedTypeKind `mkFunTy` liftedTypeKind
+  = do { let star_star_kind = liftedTypeKind `mkVisFunTy` liftedTypeKind
        ; m1_ty   <- newFlexiTyVarTy star_star_kind
        ; m2_ty   <- newFlexiTyVarTy star_star_kind
        ; tup_ty  <- newFlexiTyVarTy liftedTypeKind
@@ -635,7 +635,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap
              --                          or res                    ('by' absent)
              by_arrow = case by of
                           Nothing -> \res -> res
-                          Just {} -> \res -> (alphaTy `mkFunTy` by_e_ty) `mkFunTy` res
+                          Just {} -> \res -> (alphaTy `mkVisFunTy` by_e_ty) `mkVisFunTy` res
 
              poly_arg_ty  = m1_ty `mkAppTy` alphaTy
              using_arg_ty = m1_ty `mkAppTy` tup_ty
@@ -643,7 +643,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap
              using_res_ty = m2_ty `mkAppTy` n_app tup_ty
              using_poly_ty = mkInvForAllTy alphaTyVar $
                              by_arrow $
-                             poly_arg_ty `mkFunTy` poly_res_ty
+                             poly_arg_ty `mkVisFunTy` poly_res_ty
 
              -- 'stmts' returns a result of type (m1_ty tuple_ty),
              -- typically something like [(Int,Bool,Int)]
@@ -674,7 +674,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap
        ; new_res_ty <- newFlexiTyVarTy liftedTypeKind
        ; (_, bind_op')  <- tcSyntaxOp MCompOrigin bind_op
                              [ synKnownType using_res_ty
-                             , synKnownType (n_app tup_ty `mkFunTy` new_res_ty) ]
+                             , synKnownType (n_app tup_ty `mkVisFunTy` new_res_ty) ]
                              res_ty $ \ _ -> return ()
 
        --------------- Typecheck the 'fmap' function -------------
@@ -683,9 +683,9 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap
                        _ -> fmap unLoc . tcPolyExpr (noLoc fmap_op) $
                             mkInvForAllTy alphaTyVar $
                             mkInvForAllTy betaTyVar  $
-                            (alphaTy `mkFunTy` betaTy)
-                            `mkFunTy` (n_app alphaTy)
-                            `mkFunTy` (n_app betaTy)
+                            (alphaTy `mkVisFunTy` betaTy)
+                            `mkVisFunTy` (n_app alphaTy)
+                            `mkVisFunTy` (n_app betaTy)
 
        --------------- Typecheck the 'using' function -------------
        -- using :: ((a,b,c)->t) -> m1 (a,b,c) -> m2 (n (a,b,c))
@@ -744,14 +744,14 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap
 --        -> m (st1, (st2, st3))
 --
 tcMcStmt ctxt (ParStmt _ bndr_stmts_s mzip_op bind_op) res_ty thing_inside
-  = do { let star_star_kind = liftedTypeKind `mkFunTy` liftedTypeKind
+  = do { let star_star_kind = liftedTypeKind `mkVisFunTy` liftedTypeKind
        ; m_ty   <- newFlexiTyVarTy star_star_kind
 
        ; let mzip_ty  = mkInvForAllTys [alphaTyVar, betaTyVar] $
                         (m_ty `mkAppTy` alphaTy)
-                        `mkFunTy`
+                        `mkVisFunTy`
                         (m_ty `mkAppTy` betaTy)
-                        `mkFunTy`
+                        `mkVisFunTy`
                         (m_ty `mkAppTy` mkBoxedTupleTy [alphaTy, betaTy])
        ; mzip_op' <- unLoc `fmap` tcPolyExpr (noLoc mzip_op) mzip_ty
 
@@ -887,7 +887,7 @@ tcDoStmt ctxt (RecStmt { recS_stmts = stmts, recS_later_ids = later_names
         ; ((_, mfix_op'), mfix_res_ty)
             <- tcInferInst $ \ exp_ty ->
                tcSyntaxOp DoOrigin mfix_op
-                          [synKnownType (mkFunTy tup_ty stmts_ty)] exp_ty $
+                          [synKnownType (mkVisFunTy tup_ty stmts_ty)] exp_ty $
                \ _ -> return ()
 
         ; ((thing, new_res_ty), bind_op')
@@ -1020,7 +1020,7 @@ tcApplicativeStmts ctxt pairs rhs_ty thing_inside
       ; ts <- replicateM (arity-1) $ newInferExpTypeInst
       ; exp_tys <- replicateM arity $ newFlexiTyVarTy liftedTypeKind
       ; pat_tys <- replicateM arity $ newFlexiTyVarTy liftedTypeKind
-      ; let fun_ty = mkFunTys pat_tys body_ty
+      ; let fun_ty = mkVisFunTys pat_tys body_ty
 
        -- NB. do the <$>,<*> operators first, we don't want type errors here
        --     i.e. goOps before goArgs
index ba3603f..f24fb4a 100644 (file)
@@ -784,7 +784,7 @@ tcDataConPat penv (dL->L con_span con_name) data_con pat_ty
         { let theta'     = substTheta tenv (eqSpecPreds eq_spec ++ theta)
                            -- order is *important* as we generate the list of
                            -- dictionary binders from theta'
-              no_equalities = not (any isNomEqPred theta')
+              no_equalities = null eq_spec && not (any isEqPred theta)
               skol_info = PatSkol (RealDataCon data_con) mc
               mc = case pe_ctxt penv of
                      LamPat mc -> mc
index 822697f..d46ade1 100644 (file)
@@ -750,16 +750,16 @@ tcPatSynMatcher (dL->L loc name) lpat
                | is_unlifted = ([nlHsVar voidPrimId], [voidPrimTy])
                | otherwise   = (args,                 arg_tys)
              cont_ty = mkInfSigmaTy ex_tvs prov_theta $
-                       mkFunTys cont_arg_tys res_ty
+                       mkVisFunTys cont_arg_tys res_ty
 
-             fail_ty  = mkFunTy voidPrimTy res_ty
+             fail_ty  = mkVisFunTy voidPrimTy res_ty
 
        ; matcher_name <- newImplicitBinder name mkMatcherOcc
        ; scrutinee    <- newSysLocalId (fsLit "scrut") pat_ty
        ; cont         <- newSysLocalId (fsLit "cont")  cont_ty
        ; fail         <- newSysLocalId (fsLit "fail")  fail_ty
 
-       ; let matcher_tau   = mkFunTys [pat_ty, cont_ty, fail_ty] res_ty
+       ; let matcher_tau   = mkVisFunTys [pat_ty, cont_ty, fail_ty] res_ty
              matcher_sigma = mkInfSigmaTy (rr_tv:res_tv:univ_tvs) req_theta matcher_tau
              matcher_id    = mkExportedVanillaId matcher_name matcher_sigma
                              -- See Note [Exported LocalIds] in Id
@@ -848,8 +848,8 @@ mkPatSynBuilderId dir (dL->L _ name)
              builder_sigma  = add_void need_dummy_arg $
                               mkForAllTys univ_bndrs $
                               mkForAllTys ex_bndrs $
-                              mkFunTys theta $
-                              mkFunTys arg_tys $
+                              mkPhiTy theta $
+                              mkVisFunTys arg_tys $
                               pat_ty
              builder_id     = mkExportedVanillaId builder_name builder_sigma
               -- See Note [Exported LocalIds] in Id
@@ -956,7 +956,7 @@ tcPatSynBuilderOcc ps
 
 add_void :: Bool -> Type -> Type
 add_void need_dummy_arg ty
-  | need_dummy_arg = mkFunTy voidPrimTy ty
+  | need_dummy_arg = mkVisFunTy voidPrimTy ty
   | otherwise      = ty
 
 tcPatToExpr :: Name -> [Located Name] -> LPat GhcRn
index c76a486..76d1510 100644 (file)
@@ -2377,7 +2377,8 @@ tcRnExpr hsc_env mode rdr_expr
     _ <- perhaps_disable_default_warnings $
          simplifyInteractive residual ;
 
-    let { all_expr_ty = mkInvForAllTys qtvs (mkLamTypes dicts res_ty) } ;
+    let { all_expr_ty = mkInvForAllTys qtvs $
+                        mkPhiTy (map idType dicts) res_ty } ;
     ty <- zonkTcType all_expr_ty ;
 
     -- We normalise type families, so that the type of an expression is the
index 7c9d70e..3a7ab5b 100644 (file)
@@ -2772,7 +2772,7 @@ wrapTypeWithImplication ty impl = wrapType ty mentioned_skols givens
           mentioned_skols = filter (`elemVarSet` freeVars) skols
 
 wrapType :: Type -> [TyVar] -> [PredType] -> Type
-wrapType ty skols givens = mkSpecForAllTys skols $ mkFunTys givens ty
+wrapType ty skols givens = mkSpecForAllTys skols $ mkPhiTy givens ty
 
 
 {-
index c5ffb05..d4d3d03 100644 (file)
@@ -137,7 +137,6 @@ import qualified TcMType as TcM
 import qualified ClsInst as TcM( matchGlobalInst, ClsInstResult(..) )
 import qualified TcEnv as TcM
        ( checkWellStaged, tcGetDefaultTys, tcLookupClass, tcLookupId, topIdLvl )
-import PrelNames( heqTyConKey, eqTyConKey )
 import ClsInst( InstanceWhat(..) )
 import Kind
 import TcType
@@ -328,8 +327,7 @@ extendWorkListCt ct wl
        -> extendWorkListEq ct wl
 
      ClassPred cls _  -- See Note [Prioritise class equalities]
-       |  cls `hasKey` heqTyConKey
-       || cls `hasKey` eqTyConKey
+       |  isEqPredClass cls
        -> extendWorkListEq ct wl
 
      _ -> extendWorkListNonEq ct wl
@@ -2765,7 +2763,7 @@ checkForCyclicBinds ev_binds_map
     cycles = [c | CyclicSCC c <- stronglyConnCompFromEdgedVerticesUniq edges]
 
     coercion_cycles = [c | c <- cycles, any is_co_bind c]
-    is_co_bind (EvBind { eb_lhs = b }) = isEqPred (varType b)
+    is_co_bind (EvBind { eb_lhs = b }) = isEqPrimPred (varType b)
 
     edges :: [ Node EvVar EvBind ]
     edges = [ DigraphNode bind bndr (nonDetEltsUniqSet (evVarsOfTerm rhs))
index 65c2c60..027a401 100644 (file)
@@ -217,6 +217,7 @@ tcUserTypeSig :: SrcSpan -> LHsSigWcType GhcRn -> Maybe Name
 tcUserTypeSig loc hs_sig_ty mb_name
   | isCompleteHsSig hs_sig_ty
   = do { sigma_ty <- tcHsSigWcType ctxt_F hs_sig_ty
+       ; traceTc "tcuser" (ppr sigma_ty)
        ; return $
          CompleteSig { sig_bndr  = mkLocalId name sigma_ty
                      , sig_ctxt  = ctxt_T
@@ -449,9 +450,9 @@ tcPatSynSig name sig_ty
     build_patsyn_type kvs imp univ req ex prov body
       = mkInvForAllTys kvs $
         mkSpecForAllTys (imp ++ univ) $
-        mkFunTys req $
+        mkPhiTy req $
         mkSpecForAllTys ex $
-        mkFunTys prov $
+        mkPhiTy prov $
         body
 tcPatSynSig _ (XHsImplicitBndrs _) = panic "tcPatSynSig"
 
index 9e23eca..f50b33e 100644 (file)
@@ -1031,7 +1031,7 @@ decideMonoTyVars infer_mode name_taus psigs candidates
 
              mono_tvs1 = mono_tvs0 `unionVarSet` co_var_tvs
 
-             eq_constraints = filter isEqPred candidates
+             eq_constraints = filter isEqPrimPred candidates
              mono_tvs2      = growThetaTyVars eq_constraints mono_tvs1
 
              constrained_tvs = (growThetaTyVars eq_constraints
index 846b509..121193d 100644 (file)
@@ -1835,9 +1835,9 @@ reifyType ty@(AppTy {})     = do
     filter_out_invisible_args ty_head ty_args =
       filterByList (map isVisibleArgFlag $ appTyArgFlags ty_head ty_args)
                    ty_args
-reifyType ty@(FunTy t1 t2)
-  | isPredTy t1 = reify_for_all ty  -- Types like ((?x::Int) => Char -> Char)
-  | otherwise   = do { [r1,r2] <- reifyTypes [t1,t2] ; return (TH.ArrowT `TH.AppT` r1 `TH.AppT` r2) }
+reifyType ty@(FunTy { ft_af = af, ft_arg = t1, ft_res = t2 })
+  | InvisArg <- af = reify_for_all ty  -- Types like ((?x::Int) => Char -> Char)
+  | otherwise      = do { [r1,r2] <- reifyTypes [t1,t2] ; return (TH.ArrowT `TH.AppT` r1 `TH.AppT` r2) }
 reifyType (CastTy t _)      = reifyType t -- Casts are ignored in TH
 reifyType ty@(CoercionTy {})= noTH (sLit "coercions in types") (ppr ty)
 
@@ -1867,7 +1867,7 @@ reifyPatSynType (univTyVars, req, exTyVars, prov, argTys, resTy)
        ; req'        <- reifyCxt req
        ; exTyVars'   <- reifyTyVars exTyVars
        ; prov'       <- reifyCxt prov
-       ; tau'        <- reifyType (mkFunTys argTys resTy)
+       ; tau'        <- reifyType (mkVisFunTys argTys resTy)
        ; return $ TH.ForallT univTyVars' req'
                 $ TH.ForallT exTyVars' prov' tau' }
 
index 8dfdbb2..28b692f 100644 (file)
@@ -40,7 +40,7 @@ import TcDeriv (DerivInfo)
 import TcHsType
 import ClsInst( AssocInstInfo(..) )
 import TcMType
-import TysWiredIn ( unitTy )
+import TysWiredIn ( unitTy, makeRecoveryTyCon )
 import TcType
 import RnEnv( lookupConstructorFields )
 import FamInst
@@ -2147,8 +2147,8 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
 
        ; kvs <- kindGeneralize (mkSpecForAllTys (binderVars tmpl_bndrs) $
                                 mkSpecForAllTys exp_tvs $
-                                mkFunTys ctxt $
-                                mkFunTys arg_tys $
+                                mkPhiTy ctxt $
+                                mkVisFunTys arg_tys $
                                 unitTy)
                  -- That type is a lie, of course. (It shouldn't end in ()!)
                  -- And we could construct a proper result type from the info
@@ -2222,8 +2222,8 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
        ; let user_tvs = imp_tvs ++ exp_tvs
 
        ; tkvs <- kindGeneralize (mkSpecForAllTys user_tvs $
-                                 mkFunTys ctxt $
-                                 mkFunTys arg_tys $
+                                 mkPhiTy ctxt $
+                                 mkVisFunTys arg_tys $
                                  res_ty)
 
              -- Zonk to Types
@@ -2727,12 +2727,12 @@ checkValidTyCl :: TyCon -> TcM [TyCon]
 -- See Note [Recover from validity error]
 checkValidTyCl tc
   = setSrcSpan (getSrcSpan tc) $
-    addTyConCtxt tc $
-    recoverM recovery_code
-             (do { traceTc "Starting validity for tycon" (ppr tc)
-                 ; checkValidTyCon tc
-                 ; traceTc "Done validity for tycon" (ppr tc)
-                 ; return [tc] })
+    addTyConCtxt tc            $
+    recoverM recovery_code     $
+    do { traceTc "Starting validity for tycon" (ppr tc)
+       ; checkValidTyCon tc
+       ; traceTc "Done validity for tycon" (ppr tc)
+       ; return [tc] }
   where
     recovery_code -- See Note [Recover from validity error]
       = do { traceTc "Aborted validity for tycon" (ppr tc)
@@ -3545,7 +3545,7 @@ checkValidRoles tc
       =  check_ty_roles env role    ty1
       >> check_ty_roles env Nominal ty2
 
-    check_ty_roles env role (FunTy ty1 ty2)
+    check_ty_roles env role (FunTy ty1 ty2)
       =  check_ty_roles env role ty1
       >> check_ty_roles env role ty2
 
@@ -3709,7 +3709,7 @@ badDataConTyCon data_con res_ty_tmpl actual_res_ty
     (actual_res_tvs, actual_res_theta, actual_res_rho)
       = tcSplitNestedSigmaTys actual_res_ty
     suggested_ty = mkSpecForAllTys (actual_ex_tvs ++ actual_res_tvs) $
-                   mkFunTys (actual_theta ++ actual_res_theta)
+                   mkPhiTy (actual_theta ++ actual_res_theta)
                    actual_res_rho
 
 badGadtDecl :: Name -> SDoc
index dc983ca..e40fd3a 100644 (file)
@@ -82,14 +82,14 @@ synonymTyConsOfType ty
   = nameEnvElts (go ty)
   where
      go :: Type -> NameEnv TyCon  -- The NameEnv does duplicate elim
-     go (TyConApp tc tys)         = go_tc tc `plusNameEnv` go_s tys
-     go (LitTy _)                 = emptyNameEnv
-     go (TyVarTy _)               = emptyNameEnv
-     go (AppTy a b)               = go a `plusNameEnv` go b
-     go (FunTy a b)               = go a `plusNameEnv` go b
-     go (ForAllTy _ ty)           = go ty
-     go (CastTy ty co)            = go ty `plusNameEnv` go_co co
-     go (CoercionTy co)           = go_co co
+     go (TyConApp tc tys) = go_tc tc `plusNameEnv` go_s tys
+     go (LitTy _)         = emptyNameEnv
+     go (TyVarTy _)       = emptyNameEnv
+     go (AppTy a b)       = go a `plusNameEnv` go b
+     go (FunTy _ a b)     = go a `plusNameEnv` go b
+     go (ForAllTy _ ty)   = go ty
+     go (CastTy ty co)    = go ty `plusNameEnv` go_co co
+     go (CoercionTy co)   = go_co co
 
      -- Note [TyCon cycles through coercions?!]
      -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -598,7 +598,7 @@ irType = go
                                           lcls' = extendVarSet lcls tv
                                     ; markNominal lcls (tyVarKind tv)
                                     ; go lcls' ty }
-    go lcls (FunTy arg res)    = go lcls arg >> go lcls res
+    go lcls (FunTy _ arg res)  = go lcls arg >> go lcls res
     go _    (LitTy {})         = return ()
       -- See Note [Coercions in role inference]
     go lcls (CastTy ty _)      = go lcls ty
@@ -634,7 +634,7 @@ markNominal lcls ty = let nvars = fvVarList (FV.delFVs lcls $ get_ty_vars ty) in
     get_ty_vars :: Type -> FV
     get_ty_vars (TyVarTy tv)      = unitFV tv
     get_ty_vars (AppTy t1 t2)     = get_ty_vars t1 `unionFV` get_ty_vars t2
-    get_ty_vars (FunTy t1 t2)     = get_ty_vars t1 `unionFV` get_ty_vars t2
+    get_ty_vars (FunTy _ t1 t2)   = get_ty_vars t1 `unionFV` get_ty_vars t2
     get_ty_vars (TyConApp _ tys)  = mapUnionFV get_ty_vars tys
     get_ty_vars (ForAllTy tvb ty) = tyCoFVsBndr tvb (get_ty_vars ty)
     get_ty_vars (LitTy {})        = emptyFV
@@ -878,7 +878,7 @@ mkOneRecordSelector all_cons idDetails fl
     sel_ty | is_naughty = unitTy  -- See Note [Naughty record selectors]
            | otherwise  = mkSpecForAllTys data_tvs          $
                           mkPhiTy (conLikeStupidTheta con1) $   -- Urgh!
-                          mkFunTy data_ty                   $
+                          mkVisFunTy data_ty                $
                           mkSpecForAllTys field_tvs         $
                           mkPhiTy field_theta               $
                           -- req_theta is empty for normal DataCon
index 7fcf30a..1f6372c 100644 (file)
@@ -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
index d6b1f70..cf7700a 100644 (file)
@@ -3,12 +3,14 @@
 (c) The GRASP/AQUA Project, Glasgow University, 1992-1999
 -}
 
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE TypeFamilies #-}
 
 module TcTypeable(mkTypeableBinds) where
 
+#include "HsVersions.h"
 
 import GhcPrelude
 
@@ -432,7 +434,7 @@ typeIsTypeable ty
   | isJust (kindRep_maybe ty)       = True
 typeIsTypeable (TyVarTy _)          = True
 typeIsTypeable (AppTy a b)          = typeIsTypeable a && typeIsTypeable b
-typeIsTypeable (FunTy a b)          = typeIsTypeable a && typeIsTypeable b
+typeIsTypeable (FunTy _ a b)        = typeIsTypeable a && typeIsTypeable b
 typeIsTypeable (TyConApp tc args)   = tyConIsTypeable tc
                                    && all typeIsTypeable args
 typeIsTypeable (ForAllTy{})         = False
@@ -460,8 +462,8 @@ liftTc = KindRepM . lift
 builtInKindReps :: [(Kind, Name)]
 builtInKindReps =
     [ (star, starKindRepName)
-    , (mkFunTy star star, starArrStarKindRepName)
-    , (mkFunTys [star, star] star, starArrStarArrStarKindRepName)
+    , (mkVisFunTy star star, starArrStarKindRepName)
+    , (mkVisFunTys [star, star] star, starArrStarArrStarKindRepName)
     ]
   where
     star = liftedTypeKind
@@ -551,8 +553,9 @@ mkKindRepRhs stuff@(Stuff {..}) in_scope = new_kind_rep
         -- We handle (TYPE LiftedRep) etc separately to make it
         -- clear to consumers (e.g. serializers) that there is
         -- a loop here (as TYPE :: RuntimeRep -> TYPE 'LiftedRep)
-      | not (tcIsConstraintKind k)    -- Typeable respects the Constraint/* distinction
-                                      -- so do not follow the special case here
+      | not (tcIsConstraintKind k)
+              -- Typeable respects the Constraint/Type distinction
+              -- so do not follow the special case here
       , Just arg <- kindRep_maybe k
       , Just (tc, []) <- splitTyConApp_maybe arg
       , Just dc <- isPromotedDataCon_maybe tc
@@ -584,7 +587,7 @@ mkKindRepRhs stuff@(Stuff {..}) in_scope = new_kind_rep
     new_kind_rep (ForAllTy (Bndr var _) ty)
       = pprPanic "mkTyConKindRepBinds(ForAllTy)" (ppr var $$ ppr ty)
 
-    new_kind_rep (FunTy t1 t2)
+    new_kind_rep (FunTy t1 t2)
       = do rep1 <- getKindRep stuff in_scope t1
            rep2 <- getKindRep stuff in_scope t2
            return $ nlHsDataCon kindRepFunDataCon
index 6af873e..8a3e03c 100644 (file)
@@ -153,8 +153,8 @@ matchExpectedFunTys herald arity orig_ty thing_inside
     go acc_arg_tys n ty
       | Just ty' <- tcView ty = go acc_arg_tys n ty'
 
-    go acc_arg_tys n (FunTy arg_ty res_ty)
-      = ASSERT( not (isPredTy arg_ty) )
+    go acc_arg_tys n (FunTy { ft_af = af, ft_arg = arg_ty, ft_res = res_ty })
+      = ASSERT( af == VisArg )
         do { (result, wrap_res) <- go (mkCheckExpType arg_ty : acc_arg_tys)
                                       (n-1) res_ty
            ; return ( result
@@ -196,7 +196,7 @@ matchExpectedFunTys herald arity orig_ty thing_inside
            ; result       <- thing_inside (reverse acc_arg_tys ++ more_arg_tys) res_ty
            ; more_arg_tys <- mapM readExpType more_arg_tys
            ; res_ty       <- readExpType res_ty
-           ; let unif_fun_ty = mkFunTys more_arg_tys res_ty
+           ; let unif_fun_ty = mkVisFunTys more_arg_tys res_ty
            ; wrap <- tcSubTypeDS AppOrigin GenSigCtxt unif_fun_ty fun_ty
                          -- Not a good origin at all :-(
            ; return (result, wrap) }
@@ -282,8 +282,8 @@ matchActualFunTysPart herald ct_orig mb_thing arity orig_ty
     go n acc_args ty
       | Just ty' <- tcView ty = go n acc_args ty'
 
-    go n acc_args (FunTy arg_ty res_ty)
-      = ASSERT( not (isPredTy arg_ty) )
+    go n acc_args (FunTy { ft_af = af, ft_arg = arg_ty, ft_res = res_ty })
+      = ASSERT( af == VisArg )
         do { (wrap_res, tys, ty_r) <- go (n-1) (arg_ty : acc_args) res_ty
            ; return ( mkWpFun idHsWrapper wrap_res arg_ty ty_r doc
                     , arg_ty : tys, ty_r ) }
@@ -320,14 +320,14 @@ matchActualFunTysPart herald ct_orig mb_thing arity orig_ty
     defer n fun_ty
       = do { arg_tys <- replicateM n newOpenFlexiTyVarTy
            ; res_ty  <- newOpenFlexiTyVarTy
-           ; let unif_fun_ty = mkFunTys arg_tys res_ty
+           ; let unif_fun_ty = mkVisFunTys arg_tys res_ty
            ; co <- unifyType mb_thing fun_ty unif_fun_ty
            ; return (mkWpCastN co, arg_tys, res_ty) }
 
     ------------
     mk_ctxt :: [TcSigmaType] -> TcSigmaType -> TidyEnv -> TcM (TidyEnv, MsgDoc)
     mk_ctxt arg_tys res_ty env
-      = do { let ty = mkFunTys arg_tys res_ty
+      = do { let ty = mkVisFunTys arg_tys res_ty
            ; (env1, zonked) <- zonkTidyTcType env ty
                    -- zonking might change # of args
            ; let (zonked_args, _) = tcSplitFunTys zonked
@@ -441,7 +441,7 @@ matchExpectedAppTy orig_ty
            ; return (co, (ty1, ty2)) }
 
     orig_kind = tcTypeKind orig_ty
-    kind1 = mkFunTy liftedTypeKind orig_kind
+    kind1 = mkVisFunTy liftedTypeKind orig_kind
     kind2 = liftedTypeKind    -- m :: * -> k
                               -- arg type :: *
 
@@ -754,9 +754,8 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
     -- caused Trac #12616 because (also bizarrely) 'deriving' code had
     -- -XImpredicativeTypes on.  I deleted the entire case.
 
-    go (FunTy act_arg act_res) (FunTy exp_arg exp_res)
-      | not (isPredTy act_arg)
-      , not (isPredTy exp_arg)
+    go (FunTy { ft_af = VisArg, ft_arg = act_arg, ft_res = act_res })
+       (FunTy { ft_af = VisArg, ft_arg = exp_arg, ft_res = exp_res })
       = -- See Note [Co/contra-variance of subsumption checking]
         do { res_wrap <- tc_sub_type_ds eq_orig inst_orig  ctxt       act_res exp_res
            ; arg_wrap <- tc_sub_tc_type eq_orig given_orig GenSigCtxt exp_arg act_arg
@@ -1416,7 +1415,7 @@ uType t_or_k origin orig_ty1 orig_ty2
       | Just ty2' <- tcView ty2 = go ty1  ty2'
 
         -- Functions (or predicate functions) just check the two parts
-    go (FunTy fun1 arg1) (FunTy fun2 arg2)
+    go (FunTy _ fun1 arg1) (FunTy _ fun2 arg2)
       = do { co_l <- uType t_or_k origin fun1 fun2
            ; co_r <- uType t_or_k origin arg1 arg2
            ; return $ mkFunCo Nominal co_l co_r }
@@ -2039,7 +2038,7 @@ matchExpectedFunKind hs_ty n k = go n k
                 Indirect fun_kind -> go n fun_kind
                 Flexi ->             defer n k }
 
-    go n (FunTy arg res)
+    go n (FunTy arg res)
       = do { co <- go (n-1) res
            ; return (mkTcFunCo Nominal (mkTcNomReflCo arg) co) }
 
@@ -2049,7 +2048,7 @@ matchExpectedFunKind hs_ty n k = go n k
     defer n k
       = do { arg_kinds <- newMetaKindVars n
            ; res_kind  <- newMetaKindVar
-           ; let new_fun = mkFunTys arg_kinds res_kind
+           ; let new_fun = mkVisFunTys arg_kinds res_kind
                  origin  = TypeEqOrigin { uo_actual   = k
                                         , uo_expected = new_fun
                                         , uo_thing    = Just (ppr hs_ty)
@@ -2205,7 +2204,7 @@ preCheck dflags ty_fam_ok tv ty
       | bad_tc tc              = OC_Bad
       | otherwise              = mapM fast_check tys >> ok
     fast_check (LitTy {})      = ok
-    fast_check (FunTy a r)     = fast_check a   >> fast_check r
+    fast_check (FunTy _ a r)   = fast_check a   >> fast_check r
     fast_check (AppTy fun arg) = fast_check fun >> fast_check arg
     fast_check (CastTy ty co)  = fast_check ty  >> fast_check_co co
     fast_check (CoercionTy co) = fast_check_co co
index 218f539..8ab63f4 100644 (file)
@@ -456,13 +456,13 @@ forAllAllowed ArbitraryRank             = True
 forAllAllowed (LimitedRank forall_ok _) = forall_ok
 forAllAllowed _                         = False
 
-constraintsAllowed :: UserTypeCtxt -> Bool
--- We don't allow constraints in kinds
-constraintsAllowed (TyVarBndrKindCtxt {}) = False
-constraintsAllowed (DataKindCtxt {})      = False
-constraintsAllowed (TySynKindCtxt {})     = False
-constraintsAllowed (TyFamResKindCtxt {})  = False
-constraintsAllowed _ = True
+allConstraintsAllowed :: UserTypeCtxt -> Bool
+-- We don't allow arbitrary constraints in kinds
+allConstraintsAllowed (TyVarBndrKindCtxt {}) = False
+allConstraintsAllowed (DataKindCtxt {})      = False
+allConstraintsAllowed (TySynKindCtxt {})     = False
+allConstraintsAllowed (TyFamResKindCtxt {})  = False
+allConstraintsAllowed _ = True
 
 {-
 Note [Correctness and performance of type synonym validity checking]
@@ -615,16 +615,16 @@ check_type ve (CastTy ty _) = check_type ve ty
 --
 -- Critically, this case must come *after* the case for TyConApp.
 -- See Note [Liberal type synonyms].
-check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
-                          , ve_rank = rank, ve_expand = expand }) ty
+check_type ve@(ValidityEnv{ ve_tidy_env = env
+                          , ve_rank = rank
+                          , ve_expand = expand }) ty
   | not (null tvbs && null theta)
   = do  { traceTc "check_type" (ppr ty $$ ppr (forAllAllowed rank))
         ; checkTcM (forAllAllowed rank) (forAllTyErr env rank ty)
                 -- Reject e.g. (Maybe (?x::Int => Int)),
                 -- with a decent error message
 
-        ; checkTcM (null theta || constraintsAllowed ctxt)
-                   (constraintTyErr env ty)
+        ; checkConstraintsOK ve theta ty
                 -- Reject forall (a :: Eq b => b). blah
                 -- In a kind signature we don't allow constraints
 
@@ -650,7 +650,7 @@ check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
              | otherwise  = liftedTypeKind
         -- If there are any constraints, the kind is *. (#11405)
 
-check_type (ve@ValidityEnv{ve_rank = rank}) (FunTy arg_ty res_ty)
+check_type (ve@ValidityEnv{ve_rank = rank}) (FunTy arg_ty res_ty)
   = do  { check_type (ve{ve_rank = arg_rank}) arg_ty
         ; check_type (ve{ve_rank = res_rank}) res_ty }
   where
@@ -698,11 +698,12 @@ check_syn_tc_app (ve@ValidityEnv{ ve_ctxt = ctxt, ve_expand = expand })
 
     check_args_only, check_expansion_only :: ExpandMode -> TcM ()
     check_args_only expand = mapM_ (check_arg expand) tys
-    check_expansion_only expand =
-      case tcView ty of
-         Just ty' -> let syn_tc = fst $ tcRepSplitTyConApp ty
-                         err_ctxt = text "In the expansion of type synonym"
-                                    <+> quotes (ppr syn_tc)
+
+    check_expansion_only expand
+      = ASSERT2( isTypeSynonymTyCon tc, ppr tc )
+        case tcView ty of
+         Just ty' -> let err_ctxt = text "In the expansion of type synonym"
+                                    <+> quotes (ppr tc)
                      in addErrCtxt err_ctxt $
                         check_type (ve{ve_expand = expand}) ty'
          Nothing  -> pprPanic "check_syn_tc_app" (ppr ty)
@@ -836,6 +837,16 @@ ubxArgTyErr env ty
                       , ppr_tidy env ty ]
                 , text "Perhaps you intended to use UnboxedTuples" ] )
 
+checkConstraintsOK :: ValidityEnv -> ThetaType -> Type -> TcM ()
+checkConstraintsOK ve theta ty
+  | null theta                         = return ()
+  | allConstraintsAllowed (ve_ctxt ve) = return ()
+  | otherwise
+  = -- We are in a kind, where we allow only equality predicates
+    -- See Note [Constraints in kinds] in TyCoRep, and Trac #16263
+    checkTcM (all isEqPred theta) $
+    constraintTyErr (ve_tidy_env ve) ty
+
 constraintTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
 constraintTyErr env ty
   = (env, text "Illegal constraint in a kind:" <+> ppr_tidy env ty)
@@ -1099,8 +1110,8 @@ solved to add+canonicalise another (Foo a) constraint.  -}
 check_class_pred :: TidyEnv -> DynFlags -> UserTypeCtxt
                  -> PredType -> Class -> [TcType] -> TcM ()
 check_class_pred env dflags ctxt pred cls tys
-  |  cls `hasKey` heqTyConKey   -- (~) and (~~) are classified as classes,
-  || cls `hasKey` eqTyConKey    -- but here we want to treat them as equalities
+  |  isEqPredClass cls    -- (~) and (~~) are classified as classes,
+                          -- but here we want to treat them as equalities
   = -- pprTrace "check_class" (ppr cls) $
     check_eq_pred env dflags pred
 
@@ -1543,12 +1554,12 @@ dropCasts :: Type -> Type
 -- This function can turn a well-kinded type into an ill-kinded
 -- one, so I've kept it local to this module
 -- To consider: drop only HoleCo casts
-dropCasts (CastTy ty _)     = dropCasts ty
-dropCasts (AppTy t1 t2)     = mkAppTy (dropCasts t1) (dropCasts t2)
-dropCasts (FunTy t1 t2)     = mkFunTy (dropCasts t1) (dropCasts t2)
-dropCasts (TyConApp tc tys) = mkTyConApp tc (map dropCasts tys)
-dropCasts (ForAllTy b ty)   = ForAllTy (dropCastsB b) (dropCasts ty)
-dropCasts ty                = ty  -- LitTy, TyVarTy, CoercionTy
+dropCasts (CastTy ty _)       = dropCasts ty
+dropCasts (AppTy t1 t2)       = mkAppTy (dropCasts t1) (dropCasts t2)
+dropCasts ty@(FunTy _ t1 t2)  = ty { ft_arg = dropCasts t1, ft_res = dropCasts t2 }
+dropCasts (TyConApp tc tys)   = mkTyConApp tc (map dropCasts tys)
+dropCasts (ForAllTy b ty)     = ForAllTy (dropCastsB b) (dropCasts ty)
+dropCasts ty                  = ty  -- LitTy, TyVarTy, CoercionTy
 
 dropCastsB :: TyVarBinder -> TyVarBinder
 dropCastsB b = b   -- Don't bother in the kind of a forall
@@ -2579,7 +2590,7 @@ fvType (TyVarTy tv)          = [tv]
 fvType (TyConApp _ tys)      = fvTypes tys
 fvType (LitTy {})            = []
 fvType (AppTy fun arg)       = fvType fun ++ fvType arg
-fvType (FunTy arg res)       = fvType arg ++ fvType res
+fvType (FunTy _ arg res)     = fvType arg ++ fvType res
 fvType (ForAllTy (Bndr tv _) ty)
   = fvType (tyVarKind tv) ++
     filter (/= tv) (fvType ty)
@@ -2596,7 +2607,7 @@ sizeType (TyVarTy {})      = 1
 sizeType (TyConApp tc tys) = 1 + sizeTyConAppArgs tc tys
 sizeType (LitTy {})        = 1
 sizeType (AppTy fun arg)   = sizeType fun + sizeType arg
-sizeType (FunTy arg res)   = sizeType arg + sizeType res + 1
+sizeType (FunTy _ arg res) = sizeType arg + sizeType res + 1
 sizeType (ForAllTy _ ty)   = sizeType ty
 sizeType (CastTy ty _)     = sizeType ty
 sizeType (CoercionTy _)    = 0
@@ -2635,10 +2646,9 @@ isTerminatingClass cls
   = isIPClass cls    -- Implicit parameter constraints always terminate because
                      -- there are no instances for them --- they are only solved
                      -- by "local instances" in expressions
+    || isEqPredClass cls
     || cls `hasKey` typeableClassKey
     || cls `hasKey` coercibleTyConKey
-    || cls `hasKey` eqTyConKey
-    || cls `hasKey` heqTyConKey
 
 -- | Tidy before printing a type
 ppr_tidy :: TidyEnv -> Type -> SDoc
index 733c119..254f76c 100644 (file)
@@ -702,7 +702,7 @@ mkFunCo r co1 co2
     -- See Note [Refl invariant]
   | Just (ty1, _) <- isReflCo_maybe co1
   , Just (ty2, _) <- isReflCo_maybe co2
-  = mkReflCo r (mkFunTy ty1 ty2)
+  = mkReflCo r (mkVisFunTy ty1 ty2)
   | otherwise = FunCo r co1 co2
 
 -- | Apply a 'Coercion' to another 'Coercion'.
@@ -1900,7 +1900,7 @@ ty_co_subst lc role ty
                              liftCoSubstTyVar lc r tv
     go r (AppTy ty1 ty2)   = mkAppCo (go r ty1) (go Nominal ty2)
     go r (TyConApp tc tys) = mkTyConAppCo r tc (zipWith go (tyConRolesX r tc) tys)
-    go r (FunTy ty1 ty2)   = mkFunCo r (go r ty1) (go r ty2)
+    go r (FunTy _ ty1 ty2) = mkFunCo r (go r ty1) (go r ty2)
     go r t@(ForAllTy (Bndr v _) ty)
        = let (lc', v', h) = liftCoSubstVarBndr lc v
              body_co = ty_co_subst lc' r ty in
@@ -2196,7 +2196,7 @@ coercionKind co =
        | otherwise                = go_forall empty_subst co
        where
          empty_subst = mkEmptyTCvSubst (mkInScopeSet $ tyCoVarsOfCo co)
-    go (FunCo _ co1 co2)    = mkFunTy <$> go co1 <*> go co2
+    go (FunCo _ co1 co2)    = mkVisFunTy <$> go co1 <*> go co2
     go (CoVarCo cv)         = coVarTypes cv
     go (HoleCo h)           = coVarTypes (coHoleCoVar h)
     go (AxiomInstCo ax ind cos)
@@ -2374,7 +2374,8 @@ buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2
                   ; _           -> False      } )
         mkNomReflCo ty1
 
-    go (FunTy arg1 res1) (FunTy arg2 res2)
+    go (FunTy { ft_arg = arg1, ft_res = res1 })
+       (FunTy { ft_arg = arg2, ft_res = res2 })
       = mkFunCo Nominal (go arg1 arg2) (go res1 res2)
 
     go (TyConApp tc1 args1) (TyConApp tc2 args2)
@@ -2742,7 +2743,7 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
     go acc_xis acc_cos lc binders inner_ki _ []
       = (reverse acc_xis, reverse acc_cos, kind_co)
       where
-        final_kind = mkTyCoPiTys binders inner_ki
+        final_kind = mkPiTys binders inner_ki
         kind_co = liftCoSubst Nominal lc final_kind
 
     go acc_xis acc_cos lc (binder:binders) inner_ki (role:roles) ((xi,co):args)
index 1c9727a..88f64bf 100644 (file)
@@ -1399,11 +1399,11 @@ normalise_type ty
 
     go (AppTy ty1 ty2) = go_app_tys ty1 [ty2]
 
-    go (FunTy ty1 ty2)
+    go ty@(FunTy { ft_arg = ty1, ft_res = ty2 })
       = do { (co1, nty1) <- go ty1
            ; (co2, nty2) <- go ty2
            ; r <- getRole
-           ; return (mkFunCo r co1 co2, mkFunTy nty1 nty2) }
+           ; return (mkFunCo r co1 co2, ty { ft_arg = nty1, ft_res = nty2 }) }
     go (ForAllTy (Bndr tcvar vis) ty)
       = do { (lc', tv', h, ki') <- normalise_var_bndr tcvar
            ; (co, nty)          <- withLC lc' $ normalise_type ty
@@ -1622,9 +1622,10 @@ coreFlattenTy = go
       = let (env', tys') = coreFlattenTys env tys in
         (env', mkTyConApp tc tys')
 
-    go env (FunTy ty1 ty2) = let (env1, ty1') = go env  ty1
-                                 (env2, ty2') = go env1 ty2 in
-                             (env2, mkFunTy ty1' ty2')
+    go env ty@(FunTy { ft_arg = ty1, ft_res = ty2 })
+      = let (env1, ty1') = go env  ty1
+            (env2, ty2') = go env1 ty2 in
+        (env2, ty { ft_arg = ty1', ft_res = ty2' })
 
     go env (ForAllTy (Bndr tv vis) ty)
       = let (env1, tv') = coreFlattenVarBndr env tv
@@ -1705,7 +1706,7 @@ allTyCoVarsInTy = go
     go (TyVarTy tv)      = unitVarSet tv
     go (TyConApp _ tys)  = allTyCoVarsInTys tys
     go (AppTy ty1 ty2)   = (go ty1) `unionVarSet` (go ty2)
-    go (FunTy ty1 ty2)   = (go ty1) `unionVarSet` (go ty2)
+    go (FunTy _ ty1 ty2) = (go ty1) `unionVarSet` (go ty2)
     go (ForAllTy (Bndr tv _) ty) = unitVarSet tv     `unionVarSet`
                                    go (tyVarKind tv) `unionVarSet`
                                    go ty
index 17c8041..7989265 100644 (file)
@@ -76,7 +76,7 @@ isKindLevPoly k = ASSERT2( isLiftedTypeKind k || _is_type, ppr k )
     go AppTy{}           = True  -- it can't be a TyConApp
     go (TyConApp tc tys) = isFamilyTyCon tc || any go tys
     go ForAllTy{}        = True
-    go (FunTy t1 t2)     = go t1 || go t2
+    go (FunTy _ t1 t2)   = go t1 || go t2
     go LitTy{}           = False
     go CastTy{}          = True
     go CoercionTy{}      = True
index 0e9a599..c521a85 100644 (file)
@@ -2,10 +2,6 @@
 
 {-# LANGUAGE CPP #-}
 
--- The default iteration limit is a bit too low for the definitions
--- in this module.
-{-# OPTIONS_GHC -fmax-pmcheck-iterations=10000000 #-}
-
 module OptCoercion ( optCoercion, checkAxInstCo ) where
 
 #include "HsVersions.h"
index 9c50d2e..3594c7a 100644 (file)
@@ -17,18 +17,22 @@ Note [The Type-related module hierarchy]
 
 -- We expose the relevant stuff from this module via the Type module
 {-# OPTIONS_HADDOCK not-home #-}
-{-# LANGUAGE CPP, DeriveDataTypeable, MultiWayIf #-}
+{-# LANGUAGE CPP, DeriveDataTypeable, MultiWayIf, PatternSynonyms, BangPatterns #-}
 
 module TyCoRep (
         TyThing(..), tyThingCategory, pprTyThingCategory, pprShortTyThing,
 
         -- * Types
-        Type(..),
+        Type( TyVarTy, AppTy, TyConApp, ForAllTy
+            , LitTy, CastTy, CoercionTy
+            , FunTy, ft_arg, ft_res, ft_af
+            ),  -- Export the type synonym FunTy too
+
         TyLit(..),
         KindOrType, Kind,
         KnotTied,
         PredType, ThetaType,      -- Synonyms
-        ArgFlag(..),
+        ArgFlag(..), AnonArgFlag(..),
 
         -- * Coercions
         Coercion(..),
@@ -40,10 +44,9 @@ module TyCoRep (
         -- * Functions over types
         mkTyConTy, mkTyVarTy, mkTyVarTys,
         mkTyCoVarTy, mkTyCoVarTys,
-        mkFunTy, mkFunTys, mkTyCoForAllTy, mkForAllTys,
-        mkForAllTy,
-        mkTyCoPiTy, mkTyCoPiTys,
-        mkPiTys,
+        mkFunTy, mkVisFunTy, mkInvisFunTy, mkVisFunTys, mkInvisFunTys,
+        mkForAllTy, mkForAllTys,
+        mkPiTy, mkPiTys,
 
         kindRep_maybe, kindRep,
         isLiftedTypeKind, isUnliftedTypeKind,
@@ -58,7 +61,6 @@ module TyCoRep (
         isInvisibleArgFlag, isVisibleArgFlag,
         isInvisibleBinder, isVisibleBinder,
         isTyBinder, isNamedBinder,
-        tyCoBinderArgFlag,
 
         -- * Functions over coercions
         pickLR,
@@ -156,7 +158,7 @@ import GhcPrelude
 import {-# SOURCE #-} DataCon( dataConFullSig
                              , dataConUserTyVarBinders
                              , DataCon )
-import {-# SOURCE #-} Type( isPredTy, isCoercionTy, mkAppTy, mkCastTy
+import {-# SOURCE #-} Type( isCoercionTy, mkAppTy, mkCastTy
                           , tyCoVarsOfTypeWellScoped
                           , tyCoVarsOfTypesWellScoped
                           , scopedSort
@@ -308,7 +310,11 @@ data Type
         {-# UNPACK #-} !TyCoVarBinder
         Type            -- ^ A Π type.
 
-  | FunTy Type Type     -- ^ t1 -> t2   Very common, so an important special case
+  | FunTy      -- ^ t1 -> t2   Very common, so an important special case
+                -- See Note [Function types]
+     { ft_af  :: AnonArgFlag  -- Is this (->) or (=>)?
+     , ft_arg :: Type           -- Argument type
+     , ft_res :: Type }         -- Result type
 
   | LitTy TyLit     -- ^ Type literals are similar to type constructors.
 
@@ -327,7 +333,6 @@ data Type
 
   deriving Data.Data
 
-
 -- NOTE:  Other parts of the code assume that type literals do not contain
 -- types or type variables.
 data TyLit
@@ -335,7 +340,201 @@ data TyLit
   | StrTyLit FastString
   deriving (Eq, Ord, Data.Data)
 
-{- Note [Arguments to type constructors]
+
+{- Note [Function types]
+~~~~~~~~~~~~~~~~~~~~~~~~
+FFunTy is the constructor for a function type.  Lots of things to say
+about it!
+
+* FFunTy is the data constructor, meaning "full function type".
+
+* The function type constructor (->) has kind
+     (->) :: forall r1 r2. TYPE r1 -> TYPE r2 -> Type LiftedRep
+  mkTyConApp ensure that we convert a saturated application
+    TyConApp (->) [r1,r2,t1,t2] into FunTy t1 t2
+  dropping the 'r1' and 'r2' arguments; they are easily recovered
+  from 't1' and 't2'.
+
+* The ft_af field says whether or not this is an invisible argument
+     VisArg:   t1 -> t2    Ordinary function type
+     InvisArg: t1 => t2    t1 is guaranteed to be a predicate type,
+                           i.e. t1 :: Constraint
+  See Note [Types for coercions, predicates, and evidence]
+
+  This visibility info makes no difference in Core; it matters
+  only when we regard the type as a Haskell source type.
+
+* FunTy is a (unidirectional) pattern synonym that allows
+  positional pattern matching (FunTy arg res), ignoring the
+  ArgFlag.
+-}
+
+{- -----------------------
+      Commented out until the pattern match
+      checker can handle it; see Trac #16185
+
+      For now we use the CPP macro #define FunTy FFunTy _
+      (see HsVersions.h) to allow pattern matching on a
+      (positional) FunTy constructor.
+
+{-# COMPLETE FunTy, TyVarTy, AppTy, TyConApp
+           , ForAllTy, LitTy, CastTy, CoercionTy :: Type #-}
+
+-- | 'FunTy' is a (uni-directional) pattern synonym for the common
+-- case where we want to match on the argument/result type, but
+-- ignoring the AnonArgFlag
+pattern FunTy :: Type -> Type -> Type
+pattern FunTy arg res <- FFunTy { ft_arg = arg, ft_res = res }
+
+       End of commented out block
+---------------------------------- -}
+
+{- Note [Types for coercions, predicates, and evidence]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We treat differently:
+
+  (a) Predicate types
+        Test: isPredTy
+        Binders: DictIds
+        Kind: Constraint
+        Examples: (Eq a), and (a ~ b)
+
+  (b) Coercion types are primitive, unboxed equalities
+        Test: isCoVarTy
+        Binders: CoVars (can appear in coercions)
+        Kind: TYPE (TupleRep [])
+        Examples: (t1 ~# t2) or (t1 ~R# t2)
+
+  (c) Evidence types is the type of evidence manipulated by
+      the type constraint solver.
+        Test: isEvVarType
+        Binders: EvVars
+        Kind: Constraint or TYPE (TupleRep [])
+        Examples: all coercion types and predicate types
+
+Coercion types and predicate types are mutually exclusive,
+but evidence types are a superset of both.
+
+When treated as a user type,
+
+  - Predicates (of kind Constraint) are invisible and are
+    implicitly instantiated
+
+  - Coercion types, and non-pred evidence types (i.e. not
+    of kind Constrain), are just regular old types, are
+    visible, and are not implicitly instantiated.
+
+In a FunTy { ft_af = InvisArg }, the argument type is always
+a Predicate type.
+
+Note [Constraints in kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Do we allow a type constructor to have a kind like
+   S :: Eq a => a -> Type
+
+No, we do not.  Doing so would mean would need a TyConApp like
+   S @k @(d :: Eq k) (ty :: k)
+ and we have no way to build, or decompose, evidence like
+ (d :: Eq k) at the type level.
+
+But we admit one exception: equality.  We /do/ allow, say,
+   MkT :: (a ~ b) => a -> b -> Type a b
+
+Why?  Because we can, without much difficulty.  Moreover
+we can promote a GADT data constructor (see TyCon
+Note [Promoted data constructors]), like
+  data GT a b where
+    MkGT : a -> a -> GT a a
+so programmers might reasonably expect to be able to
+promote MkT as well.
+
+How does this work?
+
+* In TcValidity.checkConstraintsOK we reject kinds that
+  have constraints other than (a~b) and (a~~b).
+
+* In Inst.tcInstInvisibleTyBinder we instantiate a call
+  of MkT by emitting
+     [W] co :: alpha ~# beta
+  and producing the elaborated term
+     MkT @alpha @beta (Eq# alpha beta co)
+  We don't generate a boxed "Wanted"; we generate only a
+  regular old /unboxed/ primitive-equality Wanted, and build
+  the box on the spot.
+
+* How can we get such a MkT?  By promoting a GADT-style data
+  constructor
+     data T a b where
+       MkT :: (a~b) => a -> b -> T a b
+  See DataCon.mkPromotedDataCon
+  and Note [Promoted data constructors] in TyCon
+
+* We support both homogeneous (~) and heterogeneous (~~)
+  equality.  (See Note [The equality types story]
+  in TysPrim for a primer on these equality types.)
+
+* How do we prevent a MkT having an illegal constraint like
+  Eq a?  We check for this at use-sites; see TcHsType.tcTyVar,
+  specifically dc_theta_illegal_constraint.
+
+* Notice that nothing special happens if
+    K :: (a ~# b) => blah
+  because (a ~# b) is not a predicate type, and is never
+  implicitly instantiated. (Mind you, it's not clear how you
+  could creates a type constructor with such a kind.) See
+  Note [Types for coercions, predicates, and evidence]
+
+* The existence of promoted MkT with an equality-constraint
+  argument is the (only) reason that the AnonTCB constructor
+  of TyConBndrVis carries an AnonArgFlag (VisArg/InvisArg).
+  For example, when we promote the data constructor
+     MkT :: forall a b. (a~b) => a -> b -> T a b
+  we get a PromotedDataCon with tyConBinders
+      Bndr (a :: Type)  (NamedTCB Inferred)
+      Bndr (b :: Type)  (NamedTCB Inferred)
+      Bndr (_ :: a ~ b) (AnonTCB InvisArg)
+      Bndr (_ :: a)     (AnonTCB VisArg))
+      Bndr (_ :: b)     (AnonTCB VisArg))
+
+* One might reasonably wonder who *unpacks* these boxes once they are
+  made. After all, there is no type-level `case` construct. The
+  surprising answer is that no one ever does. Instead, if a GADT
+  constructor is used on the left-hand side of a type family equation,
+  that occurrence forces GHC to unify the types in question. For
+  example:
+
+  data G a where
+    MkG :: G Bool
+
+  type family F (x :: G a) :: a where
+    F MkG = False
+
+  When checking the LHS `F MkG`, GHC sees the MkG constructor and then must
+  unify F's implicit parameter `a` with Bool. This succeeds, making the equation
+
+    F Bool (MkG @Bool <Bool>) = False
+
+  Note that we never need unpack the coercion. This is because type
+  family equations are *not* parametric in their kind variables. That
+  is, we could have just said
+
+  type family H (x :: G a) :: a where
+    H _ = False
+
+  The presence of False on the RHS also forces `a` to become Bool,
+  giving us
+
+    H Bool _ = False
+
+  The fact that any of this works stems from the lack of phase
+  separation between types and kinds (unlike the very present phase
+  separation between terms and types).
+
+  Once we have the ability to pattern-match on types below top-level,
+  this will no longer cut it, but it seems fine for now.
+
+
+Note [Arguments to type constructors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Because of kind polymorphism, in addition to type application we now
 have kind instantiation. We reuse the same notations to do so.
@@ -498,13 +697,14 @@ True in any case.
 
 We decide to always construct (2) if co is not used in t.
 
-Thus in mkTyCoForAllTy, we check whether the variable is a coercion
-variable and whether it is used in the body. If so, it returns a FunTy
-instead of a ForAllTy.
+Thus in mkLamType, we check whether the variable is a coercion
+variable (of type (t1 ~# t2), and whether it is un-used in the
+body. If so, it returns a FunTy instead of a ForAllTy.
+
+There are cases we want to skip the check. For example, the check is
+unnecessary when it is known from the context that the input variable
+is a type variable.  In those cases, we use mkForAllTy.
 
-There are cases we want to skip the check. For example, the check is unnecessary
-when it is known from the context that the input variable is a type variable.
-In those cases, we use mkForAllTy.
 -}
 
 -- | A type labeled 'KnotTied' might have knot-tied tycons in it. See
@@ -522,9 +722,9 @@ type KnotTied ty = ty
 -- dependent ('Named') or nondependent ('Anon'). They may also be visible or
 -- not. See Note [TyCoBinders]
 data TyCoBinder
-  = Named TyCoVarBinder -- A type-lambda binder
-  | Anon Type           -- A term-lambda binder. Type here can be CoercionTy.
-                        -- Visibility is determined by the type (Constraint vs. *)
+  = Named TyCoVarBinder    -- A type-lambda binder
+  | Anon AnonArgFlag Type  -- A term-lambda binder. Type here can be CoercionTy.
+                           -- Visibility is determined by the AnonArgFlag
   deriving Data.Data
 
 -- | 'TyBinder' is like 'TyCoBinder', but there can only be 'TyVarBinder'
@@ -539,7 +739,8 @@ delBinderVar vars (Bndr tv _) = vars `delVarSet` tv
 -- | Does this binder bind an invisible argument?
 isInvisibleBinder :: TyCoBinder -> Bool
 isInvisibleBinder (Named (Bndr _ vis)) = isInvisibleArgFlag vis
-isInvisibleBinder (Anon ty)            = isPredTy ty
+isInvisibleBinder (Anon InvisArg _)    = True
+isInvisibleBinder (Anon VisArg   _)    = False
 
 -- | Does this binder bind a visible argument?
 isVisibleBinder :: TyCoBinder -> Bool
@@ -558,12 +759,6 @@ isTyBinder :: TyCoBinder -> Bool
 isTyBinder (Named bnd) = isTyVarBinder bnd
 isTyBinder _ = True
 
-tyCoBinderArgFlag :: TyCoBinder -> ArgFlag
-tyCoBinderArgFlag (Named (Bndr _ flag)) = flag
-tyCoBinderArgFlag (Anon ty)
- | isPredTy ty = Inferred
- | otherwise = Required
-
 {- Note [TyCoBinders]
 ~~~~~~~~~~~~~~~~~~~
 A ForAllTy contains a TyCoVarBinder.  But a type can be decomposed
@@ -815,26 +1010,19 @@ mkTyCoVarTy v
 mkTyCoVarTys :: [TyCoVar] -> [Type]
 mkTyCoVarTys = map mkTyCoVarTy
 
-infixr 3 `mkFunTy`      -- Associates to the right
--- | Make an arrow type
-mkFunTy :: Type -> Type -> Type
-mkFunTy arg res = FunTy arg res
+infixr 3 `mkFunTy`, `mkVisFunTy`, `mkInvisFunTy`      -- Associates to the right
 
--- | Make nested arrow types
-mkFunTys :: [Type] -> Type -> Type
-mkFunTys tys ty = foldr mkFunTy ty tys
+mkFunTy :: AnonArgFlag -> Type -> Type -> Type
+mkFunTy af arg res = FunTy { ft_af = af, ft_arg = arg, ft_res = res }
 
--- | If tv is a coercion variable and it is not used in the body, returns
--- a FunTy, otherwise makes a forall type.
--- See Note [Unused coercion variable in ForAllTy]
-mkTyCoForAllTy :: TyCoVar -> ArgFlag -> Type -> Type
-mkTyCoForAllTy tv vis ty
-  | isCoVar tv
-  , not (tv `elemVarSet` tyCoVarsOfType ty)
-  = ASSERT( vis == Inferred )
-    mkFunTy (varType tv) ty
-  | otherwise
-  = ForAllTy (Bndr tv vis) ty
+mkVisFunTy, mkInvisFunTy :: Type -> Type -> Type
+mkVisFunTy   = mkFunTy VisArg
+mkInvisFunTy = mkFunTy InvisArg
+
+-- | Make nested arrow types
+mkVisFunTys, mkInvisFunTys :: [Type] -> Type -> Type
+mkVisFunTys   tys ty = foldr mkVisFunTy   ty tys
+mkInvisFunTys tys ty = foldr mkInvisFunTy ty tys
 
 -- | Like 'mkTyCoForAllTy', but does not check the occurrence of the binder
 -- See Note [Unused coercion variable in ForAllTy]
@@ -845,19 +1033,10 @@ mkForAllTy tv vis ty = ForAllTy (Bndr tv vis) ty
 mkForAllTys :: [TyCoVarBinder] -> Type -> Type
 mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
 
-mkTyCoPiTy :: TyCoBinder -> Type -> Type
-mkTyCoPiTy (Anon ty1) ty2           = FunTy ty1 ty2
-mkTyCoPiTy (Named (Bndr tv vis)) ty = mkTyCoForAllTy tv vis ty
-
--- | Like 'mkTyCoPiTy', but does not check the occurrence of the binder
 mkPiTy:: TyCoBinder -> Type -> Type
-mkPiTy (Anon ty1) ty2           = FunTy ty1 ty2
+mkPiTy (Anon af ty1) ty2        = FunTy { ft_af = af, ft_arg = ty1, ft_res = ty2 }
 mkPiTy (Named (Bndr tv vis)) ty = mkForAllTy tv vis ty
 
-mkTyCoPiTys :: [TyCoBinder] -> Type -> Type
-mkTyCoPiTys tbs ty = foldr mkTyCoPiTy ty tbs
-
--- | Like 'mkTyCoPiTys', but does not check the occurrence of the binder
 mkPiTys :: [TyCoBinder] -> Type -> Type
 mkPiTys tbs ty = foldr mkPiTy ty tbs
 
@@ -1004,6 +1183,11 @@ data Coercion
 
   | FunCo Role Coercion Coercion         -- lift FunTy
          -- FunCo :: "e" -> e -> e -> e
+         -- Note: why doesn't FunCo have a AnonArgFlag, like FunTy?
+         -- Because the AnonArgFlag has no impact on Core; it is only
+         -- there to guide implicit instantiation of Haskell source
+         -- types, and that is irrelevant for coercions, which are
+         -- Core-only.
 
   -- These are special
   | CoVarCo CoVar      -- :: _ -> (N or R)
@@ -1758,7 +1942,7 @@ ty_co_vars_of_type (TyVarTy v) is acc
 ty_co_vars_of_type (TyConApp _ tys)   is acc = ty_co_vars_of_types tys is acc
 ty_co_vars_of_type (LitTy {})         _  acc = acc
 ty_co_vars_of_type (AppTy fun arg)    is acc = ty_co_vars_of_type fun is (ty_co_vars_of_type arg is acc)
-ty_co_vars_of_type (FunTy arg res)    is acc = ty_co_vars_of_type arg is (ty_co_vars_of_type res is acc)
+ty_co_vars_of_type (FunTy _ arg res)  is acc = ty_co_vars_of_type arg is (ty_co_vars_of_type res is acc)
 ty_co_vars_of_type (ForAllTy (Bndr tv _) ty) is acc = ty_co_vars_of_type (varType tv) is $
                                                       ty_co_vars_of_type ty (extendVarSet is tv) acc
 ty_co_vars_of_type (CastTy ty co)     is acc = ty_co_vars_of_type ty is (ty_co_vars_of_co co is acc)
@@ -1895,7 +2079,7 @@ tyCoFVsOfType (TyVarTy v)        f bound_vars (acc_list, acc_set)
 tyCoFVsOfType (TyConApp _ tys)   f bound_vars acc = tyCoFVsOfTypes tys f bound_vars acc
 tyCoFVsOfType (LitTy {})         f bound_vars acc = emptyFV f bound_vars acc
 tyCoFVsOfType (AppTy fun arg)    f bound_vars acc = (tyCoFVsOfType fun `unionFV` tyCoFVsOfType arg) f bound_vars acc
-tyCoFVsOfType (FunTy arg res)    f bound_vars acc = (tyCoFVsOfType arg `unionFV` tyCoFVsOfType res) f bound_vars acc
+tyCoFVsOfType (FunTy _ arg res)  f bound_vars acc = (tyCoFVsOfType arg `unionFV` tyCoFVsOfType res) f bound_vars acc
 tyCoFVsOfType (ForAllTy bndr ty) f bound_vars acc = tyCoFVsBndr bndr (tyCoFVsOfType ty)  f bound_vars acc
 tyCoFVsOfType (CastTy ty co)     f bound_vars acc = (tyCoFVsOfType ty `unionFV` tyCoFVsOfCo co) f bound_vars acc
 tyCoFVsOfType (CoercionTy co)    f bound_vars acc = tyCoFVsOfCo co f bound_vars acc
@@ -2090,7 +2274,7 @@ almost_devoid_co_var_of_type (LitTy {}) _ = True
 almost_devoid_co_var_of_type (AppTy fun arg) cv
   = almost_devoid_co_var_of_type fun cv
   && almost_devoid_co_var_of_type arg cv
-almost_devoid_co_var_of_type (FunTy arg res) cv
+almost_devoid_co_var_of_type (FunTy arg res) cv
   = almost_devoid_co_var_of_type arg cv
   && almost_devoid_co_var_of_type res cv
 almost_devoid_co_var_of_type (ForAllTy (Bndr v _) ty) cv
@@ -2128,12 +2312,12 @@ almost_devoid_co_var_of_types (ty:tys) cv
 injectiveVarsOfType :: Type -> FV
 injectiveVarsOfType = go
   where
-    go ty                | Just ty' <- coreView ty
-                         = go ty'
-    go (TyVarTy v)       = unitFV v `unionFV` go (tyVarKind v)
-    go (AppTy f a)       = go f `unionFV` go a
-    go (FunTy ty1 ty2)   = go ty1 `unionFV` go ty2
-    go (TyConApp tc tys) =
+    go ty                 | Just ty' <- coreView ty
+                          = go ty'
+    go (TyVarTy v)        = unitFV v `unionFV` go (tyVarKind v)
+    go (AppTy f a)        = go f `unionFV` go a
+    go (FunTy _ ty1 ty2)  = go ty1 `unionFV` go ty2
+    go (TyConApp tc tys)  =
       case tyConInjectivityInfo tc of
         NotInjective  -> emptyFV
         Injective inj -> mapUnionFV go $
@@ -2156,7 +2340,8 @@ injectiveVarsOfType = go
 -- files.
 tyConAppNeedsKindSig
   :: Bool  -- ^ Should specified binders count towards injective positions in
-           --   the kind of the TyCon?
+           --   the kind of the TyCon? (If you're using visible kind
+           --   applications, then you want True here.
   -> TyCon
   -> Int   -- ^ The number of args the 'TyCon' is applied to.
   -> Bool  -- ^ Does @T t_1 ... t_n@ need a kind signature? (Where @n@ is the
@@ -2170,8 +2355,7 @@ tyConAppNeedsKindSig spec_inj_pos tc n_args
         result_kind  = mkTyConKind remaining_binders tc_res_kind
         result_vars  = tyCoVarsOfType result_kind
         dropped_vars = fvVarSet $
-                       mapUnionFV (injective_vars_of_binder spec_inj_pos)
-                                  dropped_binders
+                       mapUnionFV injective_vars_of_binder dropped_binders
 
     in not (subVarSet result_vars dropped_vars)
   where
@@ -2181,20 +2365,17 @@ tyConAppNeedsKindSig spec_inj_pos tc n_args
     -- Returns the variables that would be fixed by knowing a TyConBinder. See
     -- Note [When does a tycon application need an explicit kind signature?]
     -- for a more detailed explanation of what this function does.
-    injective_vars_of_binder
-      :: Bool -- Should specified binders count towards injective positions?
-              -- (If you're using visible kind applications, then you want True
-              -- here.)
-      -> TyConBinder -> FV
-    injective_vars_of_binder spec_inj_pos (Bndr tv vis) =
+    injective_vars_of_binder :: TyConBinder -> FV
+    injective_vars_of_binder (Bndr tv vis) =
       case vis of
-        AnonTCB -> injectiveVarsOfType (varType tv)
-        NamedTCB argf
-          |     (argf == Required)
-             || (spec_inj_pos && (argf == Specified))
-          -> unitFV tv `unionFV` injectiveVarsOfType (varType tv)
-          |  otherwise
-          -> emptyFV
+        AnonTCB VisArg -> injectiveVarsOfType (varType tv)
+        NamedTCB argf  | source_of_injectivity argf
+                       -> unitFV tv `unionFV` injectiveVarsOfType (varType tv)
+        _              -> emptyFV
+
+    source_of_injectivity Required  = True
+    source_of_injectivity Specified = spec_inj_pos
+    source_of_injectivity Inferred  = False
 
 {-
 Note [When does a tycon application need an explicit kind signature?]
@@ -2427,7 +2608,7 @@ noFreeVarsOfType (TyVarTy _)      = False
 noFreeVarsOfType (AppTy t1 t2)    = noFreeVarsOfType t1 && noFreeVarsOfType t2
 noFreeVarsOfType (TyConApp _ tys) = all noFreeVarsOfType tys
 noFreeVarsOfType ty@(ForAllTy {}) = isEmptyVarSet (tyCoVarsOfType ty)
-noFreeVarsOfType (FunTy t1 t2)    = noFreeVarsOfType t1 && noFreeVarsOfType t2
+noFreeVarsOfType (FunTy _ t1 t2)  = noFreeVarsOfType t1 && noFreeVarsOfType t2
 noFreeVarsOfType (LitTy _)        = True
 noFreeVarsOfType (CastTy ty co)   = noFreeVarsOfType ty && noFreeVarsOfCo co
 noFreeVarsOfType (CoercionTy co)  = noFreeVarsOfCo co
@@ -2728,7 +2909,7 @@ extendTvSubstBinderAndInScope :: TCvSubst -> TyCoBinder -> Type -> TCvSubst
 extendTvSubstBinderAndInScope subst (Named (Bndr v _)) ty
   = ASSERT( isTyVar v )
     extendTvSubstAndInScope subst v ty
-extendTvSubstBinderAndInScope subst (Anon _)     _
+extendTvSubstBinderAndInScope subst (Anon {}) _
   = subst
 
 extendTvSubstWithClone :: TCvSubst -> TyVar -> TyVar -> TCvSubst
@@ -3108,7 +3289,10 @@ subst_ty subst ty
                 -- by [Int], represented with TyConApp
     go (TyConApp tc tys) = let args = map go tys
                            in  args `seqList` TyConApp tc args
-    go (FunTy arg res)   = (FunTy $! go arg) $! go res
+    go ty@(FunTy { ft_arg = arg, ft_res = res })
+      = let !arg' = go arg
+            !res' = go res
+        in ty { ft_arg = arg', ft_res = res' }
     go (ForAllTy (Bndr tv vis) ty)
                          = case substVarBndrUnchecked subst tv of
                              (subst', tv') ->
@@ -3561,7 +3745,7 @@ pprTyVar tv
     kind = tyVarKind tv
 
 instance Outputable TyCoBinder where
-  ppr (Anon ty) = text "[anon]" <+> ppr ty
+  ppr (Anon af ty) = ppr af <+> ppr ty
   ppr (Named (Bndr v Required))  = ppr v
   ppr (Named (Bndr v Specified)) = char '@' <> ppr v
   ppr (Named (Bndr v Inferred))  = braces (ppr v)
@@ -3586,9 +3770,13 @@ debug_ppr_ty _ (LitTy l)
 debug_ppr_ty _ (TyVarTy tv)
   = ppr tv  -- With -dppr-debug we get (tv :: kind)
 
-debug_ppr_ty prec (FunTy arg res)
+debug_ppr_ty prec (FunTy { ft_af = af, ft_arg = arg, ft_res = res })
   = maybeParen prec funPrec $
     sep [debug_ppr_ty funPrec arg, arrow <+> debug_ppr_ty prec res]
+  where
+    arrow = case af of
+              VisArg   -> text "->"
+              InvisArg -> text "=>"
 
 debug_ppr_ty prec (TyConApp tc tys)
   | null tys  = ppr tc
@@ -3789,13 +3977,15 @@ tidyTypes env tys = map (tidyType env) tys
 
 ---------------
 tidyType :: TidyEnv -> Type -> Type
-tidyType _   (LitTy n)            = LitTy n
-tidyType env (TyVarTy tv)         = TyVarTy (tidyTyCoVarOcc env tv)
-tidyType env (TyConApp tycon tys) = let args = tidyTypes env tys
-                                    in args `seqList` TyConApp tycon args
-tidyType env (AppTy fun arg)      = (AppTy $! (tidyType env fun)) $! (tidyType env arg)
-tidyType env (FunTy fun arg)      = (FunTy $! (tidyType env fun)) $! (tidyType env arg)
-tidyType env (ty@(ForAllTy{}))    = mkForAllTys' (zip tvs' vis) $! tidyType env' body_ty
+tidyType _   (LitTy n)             = LitTy n
+tidyType env (TyVarTy tv)          = TyVarTy (tidyTyCoVarOcc env tv)
+tidyType env (TyConApp tycon tys)  = let args = tidyTypes env tys
+                                     in args `seqList` TyConApp tycon args
+tidyType env (AppTy fun arg)       = (AppTy $! (tidyType env fun)) $! (tidyType env arg)
+tidyType env ty@(FunTy _ arg res)  = let { !arg' = tidyType env arg
+                                         ; !res' = tidyType env res }
+                                     in ty { ft_arg = arg', ft_res = res' }
+tidyType env (ty@(ForAllTy{}))     = mkForAllTys' (zip tvs' vis) $! tidyType env' body_ty
   where
     (tvs, vis, body_ty) = splitForAllTys' ty
     (env', tvs') = tidyVarBndrs env tvs
@@ -3917,7 +4107,7 @@ typeSize :: Type -> Int
 typeSize (LitTy {})                 = 1
 typeSize (TyVarTy {})               = 1
 typeSize (AppTy t1 t2)              = typeSize t1 + typeSize t2
-typeSize (FunTy t1 t2)              = typeSize t1 + typeSize t2
+typeSize (FunTy _ t1 t2)            = typeSize t1 + typeSize t2
 typeSize (ForAllTy (Bndr tv _) t)   = typeSize (varType tv) + typeSize t
 typeSize (TyConApp _ ts)            = 1 + sum (map typeSize ts)
 typeSize (CastTy ty co)             = typeSize ty + coercionSize co
index 5af8c1d..cdc4cd6 100644 (file)
@@ -4,6 +4,7 @@ import GhcPrelude
 
 import Outputable ( SDoc )
 import Data.Data  ( Data )
+import {-# SOURCE #-} Var( Var, ArgFlag, AnonArgFlag )
 
 data Type
 data TyThing
@@ -22,8 +23,9 @@ type MCoercionN = MCoercion
 
 pprKind :: Kind -> SDoc
 pprType :: Type -> SDoc
+mkFunTy   :: AnonArgFlag -> Type -> Type -> Type
+mkForAllTy :: Var -> ArgFlag -> Type -> Type
 
 isRuntimeRepTy :: Type -> Bool
 
-instance Data Type
-  -- To support Data instances in CoAxiom
+instance Data Type  -- To support Data instances in CoAxiom
index ca49560..4557ad6 100644 (file)
@@ -104,7 +104,6 @@ module TyCon(
 
         -- ** Manipulating TyCons
         expandSynTyCon_maybe,
-        makeRecoveryTyCon,
         newTyConCo, newTyConCo_maybe,
         pprPromotionQuote, mkTyConKind,
 
@@ -133,10 +132,9 @@ module TyCon(
 
 import GhcPrelude
 
-import {-# SOURCE #-} TyCoRep    ( Kind, Type, PredType, pprType )
+import {-# SOURCE #-} TyCoRep    ( Kind, Type, PredType, pprType, mkForAllTy, mkFunTy )
 import {-# SOURCE #-} TysWiredIn ( runtimeRepTyCon, constraintKind
-                                 , vecCountTyCon, vecElemTyCon, liftedTypeKind
-                                 , mkFunKind, mkForAllKind )
+                                 , vecCountTyCon, vecElemTyCon, liftedTypeKind )
 import {-# SOURCE #-} DataCon    ( DataCon, dataConExTyCoVars, dataConFieldLabels
                                  , dataConTyCon, dataConFullSig
                                  , isUnboxedSumCon )
@@ -403,18 +401,18 @@ type TyConTyCoBinder = VarBndr TyCoVar TyConBndrVis
 
 data TyConBndrVis
   = NamedTCB ArgFlag
-  | AnonTCB
+  | AnonTCB  AnonArgFlag
 
 instance Outputable TyConBndrVis where
-  ppr (NamedTCB flag) = text "NamedTCB" <+> ppr flag
-  ppr AnonTCB         = text "AnonTCB"
+  ppr (NamedTCB flag) = text "NamedTCB" <> ppr flag
+  ppr (AnonTCB af)    = text "AnonTCB"  <> ppr af
 
-mkAnonTyConBinder :: TyVar -> TyConBinder
-mkAnonTyConBinder tv = ASSERT( isTyVar tv)
-                       Bndr tv AnonTCB
+mkAnonTyConBinder :: AnonArgFlag -> TyVar -> TyConBinder
+mkAnonTyConBinder af tv = ASSERT( isTyVar tv)
+                          Bndr tv (AnonTCB af)
 
-mkAnonTyConBinders :: [TyVar] -> [TyConBinder]
-mkAnonTyConBinders tvs = map mkAnonTyConBinder tvs
+mkAnonTyConBinders :: AnonArgFlag -> [TyVar] -> [TyConBinder]
+mkAnonTyConBinders af tvs = map (mkAnonTyConBinder af) tvs
 
 mkNamedTyConBinder :: ArgFlag -> TyVar -> TyConBinder
 -- The odd argument order supports currying
@@ -432,14 +430,15 @@ mkRequiredTyConBinder :: TyCoVarSet  -- these are used dependently
                       -> TyConBinder
 mkRequiredTyConBinder dep_set tv
   | tv `elemVarSet` dep_set = mkNamedTyConBinder Required tv
-  | otherwise               = mkAnonTyConBinder tv
+  | otherwise               = mkAnonTyConBinder  VisArg   tv
 
 tyConBinderArgFlag :: TyConBinder -> ArgFlag
 tyConBinderArgFlag (Bndr _ vis) = tyConBndrVisArgFlag vis
 
 tyConBndrVisArgFlag :: TyConBndrVis -> ArgFlag
-tyConBndrVisArgFlag (NamedTCB vis) = vis
-tyConBndrVisArgFlag AnonTCB        = Required
+tyConBndrVisArgFlag (NamedTCB vis)     = vis
+tyConBndrVisArgFlag (AnonTCB VisArg)   = Required
+tyConBndrVisArgFlag (AnonTCB InvisArg) = Inferred    -- See Note [AnonTCB InvisArg]
 
 isNamedTyConBinder :: TyConBinder -> Bool
 -- Identifies kind variables
@@ -453,8 +452,9 @@ isVisibleTyConBinder :: VarBndr tv TyConBndrVis -> Bool
 isVisibleTyConBinder (Bndr _ tcb_vis) = isVisibleTcbVis tcb_vis
 
 isVisibleTcbVis :: TyConBndrVis -> Bool
-isVisibleTcbVis (NamedTCB vis) = isVisibleArgFlag vis
-isVisibleTcbVis AnonTCB        = True
+isVisibleTcbVis (NamedTCB vis)     = isVisibleArgFlag vis
+isVisibleTcbVis (AnonTCB VisArg)   = True
+isVisibleTcbVis (AnonTCB InvisArg) = False
 
 isInvisibleTyConBinder :: VarBndr tv TyConBndrVis -> Bool
 -- Works for IfaceTyConBinder too
@@ -464,8 +464,8 @@ mkTyConKind :: [TyConBinder] -> Kind -> Kind
 mkTyConKind bndrs res_kind = foldr mk res_kind bndrs
   where
     mk :: TyConBinder -> Kind -> Kind
-    mk (Bndr tv AnonTCB)        k = mkFunKind (varType tv) k
-    mk (Bndr tv (NamedTCB vis)) k = mkForAllKind tv vis k
+    mk (Bndr tv (AnonTCB af))   k = mkFunTy af (varType tv) k
+    mk (Bndr tv (NamedTCB vis)) k = mkForAllTy tv vis k
 
 tyConTyVarBinders :: [TyConBinder]   -- From the TyCon
                   -> [TyVarBinder]   -- Suitable for the foralls of a term function
@@ -476,7 +476,8 @@ tyConTyVarBinders tc_bndrs
    mk_binder (Bndr tv tc_vis) = mkTyVarBinder vis tv
       where
         vis = case tc_vis of
-                AnonTCB           -> Specified
+                AnonTCB VisArg    -> Specified
+                AnonTCB InvisArg  -> Inferred   -- See Note [AnonTCB InvisArg]
                 NamedTCB Required -> Specified
                 NamedTCB vis      -> vis
 
@@ -486,7 +487,26 @@ tyConVisibleTyVars tc
   = [ tv | Bndr tv vis <- tyConBinders tc
          , isVisibleTcbVis vis ]
 
-{- Note [Building TyVarBinders from TyConBinders]
+{- Note [AnonTCB InivsArg]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+It's pretty rare to have an (AnonTCB InvisArg) binder.  The
+only way it can occur is in a PromotedDataCon whose
+kind has an equality constraint:
+  'MkT :: forall a b. (a~b) => blah
+See Note [Constraints in kinds] in TyCoRep, and
+Note [Promoted data constructors] in this module.
+
+When mapping an (AnonTCB InvisArg) to an ArgFlag, in
+tyConBndrVisArgFlag, we use "Inferred" to mean "the user cannot
+specify this arguments, even with visible type/kind application;
+instead the type checker must fill it in.
+
+We map (AnonTCB VisArg) to Required, of course: the user must
+provide it. It would be utterly wrong to do this for constraint
+arguments, which is why AnonTCB must have the AnonArgFlag in
+the first place.
+
+Note [Building TyVarBinders from TyConBinders]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We sometimes need to build the quantified type of a value from
 the TyConBinders of a type or class.  For that we need not
@@ -597,18 +617,21 @@ They fit together like so:
 -}
 
 instance Outputable tv => Outputable (VarBndr tv TyConBndrVis) where
-  ppr (Bndr v AnonTCB)              = text "anon" <+> parens (ppr v)
-  ppr (Bndr v (NamedTCB Required))  = text "req"  <+> parens (ppr v)
-  ppr (Bndr v (NamedTCB Specified)) = text "spec" <+> parens (ppr v)
-  ppr (Bndr v (NamedTCB Inferred))  = text "inf"  <+> parens (ppr v)
+  ppr (Bndr v bi) = ppr_bi bi <+> parens (ppr v)
+    where
+      ppr_bi (AnonTCB VisArg)     = text "anon-vis"
+      ppr_bi (AnonTCB InvisArg)   = text "anon-invis"
+      ppr_bi (NamedTCB Required)  = text "req"
+      ppr_bi (NamedTCB Specified) = text "spec"
+      ppr_bi (NamedTCB Inferred)  = text "inf"
 
 instance Binary TyConBndrVis where
-  put_ bh AnonTCB        = putByte bh 0
+  put_ bh (AnonTCB af)   = do { putByte bh 0; put_ bh af }
   put_ bh (NamedTCB vis) = do { putByte bh 1; put_ bh vis }
 
   get bh = do { h <- getByte bh
               ; case h of
-                  0 -> return AnonTCB
+                  0 -> do { af  <- get bh; return (AnonTCB af) }
                   _ -> do { vis <- get bh; return (NamedTCB vis) } }
 
 
@@ -1119,12 +1142,20 @@ via the PromotedDataCon alternative in TyCon.
   the DataCon.  Eg. If the data constructor Data.Maybe.Just(unique 78,
   say) is promoted to a TyCon whose name is Data.Maybe.Just(unique 78)
 
-* Small note: We promote the *user* type of the DataCon.  Eg
+* We promote the *user* type of the DataCon.  Eg
      data T = MkT {-# UNPACK #-} !(Bool, Bool)
   The promoted kind is
-     MkT :: (Bool,Bool) -> T
+     'MkT :: (Bool,Bool) -> T
+  *not*
+     'MkT :: Bool -> Bool -> T
+
+* Similarly for GADTs:
+     data G a where
+       MkG :: forall b. b -> G [b]
+  The promoted data constructor has kind
+       'MkG :: forall b. b -> G [b]
   *not*
-     MkT :: Bool -> Bool -> T
+       'MkG :: forall a b. (a ~# [b]) => b -> G a
 
 Note [Enumeration types]
 ~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1712,16 +1743,6 @@ isAbstractTyCon :: TyCon -> Bool
 isAbstractTyCon (AlgTyCon { algTcRhs = AbstractTyCon }) = True
 isAbstractTyCon _ = False
 
--- | Make a fake, recovery 'TyCon' from an existing one.
--- Used when recovering from errors
-makeRecoveryTyCon :: TyCon -> TyCon
-makeRecoveryTyCon tc
-  = mkTcTyCon (tyConName tc)
-              (tyConBinders tc) (tyConResKind tc)
-              [{- no scoped vars -}]
-              True
-              (tyConFlavour tc)
-
 -- | Does this 'TyCon' represent something that cannot be defined in Haskell?
 isPrimTyCon :: TyCon -> Bool
 isPrimTyCon (PrimTyCon {}) = True
index 945d7e1..473e9e5 100644 (file)
@@ -14,7 +14,8 @@ module Type (
         -- $type_classification
 
         -- $representation_types
-        TyThing(..), Type, ArgFlag(..), KindOrType, PredType, ThetaType,
+        TyThing(..), Type, ArgFlag(..), AnonArgFlag,
+        KindOrType, PredType, ThetaType,
         Var, TyVar, isTyVar, TyCoVar, TyCoBinder, TyCoVarBinder, TyVarBinder,
         KnotTied,
 
@@ -25,14 +26,15 @@ module Type (
         mkAppTy, mkAppTys, splitAppTy, splitAppTys, repSplitAppTys,
         splitAppTy_maybe, repSplitAppTy_maybe, tcRepSplitAppTy_maybe,
 
-        mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe,
+        mkVisFunTy, mkInvisFunTy, mkVisFunTys, mkInvisFunTys,
+        splitFunTy, splitFunTy_maybe,
         splitFunTys, funResultTy, funArgTy,
 
         mkTyConApp, mkTyConTy,
         tyConAppTyCon_maybe, tyConAppTyConPicky_maybe,
         tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs,
         splitTyConApp_maybe, splitTyConApp, tyConAppArgN, nextRole,
-        tcRepSplitTyConApp_maybe, tcRepSplitTyConApp, tcSplitTyConApp_maybe,
+        tcSplitTyConApp_maybe,
         splitListTyConApp_maybe,
         repSplitTyConApp_maybe,
 
@@ -44,8 +46,8 @@ module Type (
         splitForAllTy_maybe, splitForAllTy,
         splitForAllTy_ty_maybe, splitForAllTy_co_maybe,
         splitPiTy_maybe, splitPiTy, splitPiTys,
-        mkTyCoPiTy, mkTyCoPiTys, mkTyConBindersPreferAnon,
-        mkPiTys,
+        mkTyConBindersPreferAnon,
+        mkPiTy, mkPiTys,
         mkLamType, mkLamTypes,
         piResultTy, piResultTys,
         applyTysX, dropForAlls,
@@ -85,7 +87,7 @@ module Type (
         equalityTyCon,
         mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
         mkClassPred,
-        isClassPred, isEqPred, isNomEqPred,
+        isClassPred, isEqPrimPred, isEqPred, isEqPredClass,
         isIPPred, isIPPred_maybe, isIPTyCon, isIPClass,
         isCTupleClass,
 
@@ -104,7 +106,7 @@ module Type (
         binderVar, binderVars, binderType, binderArgFlag,
         tyCoBinderType, tyCoBinderVar_maybe,
         tyBinderType,
-        binderRelevantType_maybe, caseBinder,
+        binderRelevantType_maybe,
         isVisibleArgFlag, isInvisibleArgFlag, isVisibleBinder,
         isInvisibleBinder, isNamedBinder,
         tyConBindersTyCoBinders,
@@ -423,8 +425,8 @@ expandTypeSynonyms ty
     go _     (LitTy l)     = LitTy l
     go subst (TyVarTy tv)  = substTyVar subst tv
     go subst (AppTy t1 t2) = mkAppTy (go subst t1) (go subst t2)
-    go subst (FunTy arg res)
-      = mkFunTy (go subst arg) (go subst res)
+    go subst ty@(FunTy _ arg res)
+      = ty { ft_arg = go subst arg, ft_res = go subst res }
     go subst (ForAllTy (Bndr tv vis) t)
       = let (subst', tv') = substVarBndrUsing go subst tv in
         ForAllTy (Bndr tv' vis) (go subst' t)
@@ -552,8 +554,16 @@ mapType mapper@(TyCoMapper { tcm_tyvar = tyvar
         env ty
   = go ty
   where
-    go (TyVarTy tv) = tyvar env tv
-    go (AppTy t1 t2) = mkAppTy <$> go t1 <*> go t2
+    go (TyVarTy tv)    = tyvar env tv
+    go (AppTy t1 t2)   = mkAppTy <$> go t1 <*> go t2
+    go ty@(LitTy {})   = return ty
+    go (CastTy ty co)  = mkCastTy <$> go ty <*> mapCoercion mapper env co
+    go (CoercionTy co) = CoercionTy <$> mapCoercion mapper env co
+
+    go ty@(FunTy _ arg res)
+      = do { arg' <- go arg; res' <- go res
+           ; return (ty { ft_arg = arg', ft_res = res' }) }
+
     go ty@(TyConApp tc tys)
       | isTcTyCon tc
       = do { tc' <- tycon tc
@@ -566,14 +576,10 @@ mapType mapper@(TyCoMapper { tcm_tyvar = tyvar
       | otherwise
       = mkTyConApp tc <$> mapM go tys
 
-    go (FunTy arg res)   = FunTy <$> go arg <*> go res
     go (ForAllTy (Bndr tv vis) inner)
       = do { (env', tv') <- tycobinder env tv vis
            ; inner' <- mapType mapper env' inner
            ; return $ ForAllTy (Bndr tv' vis) inner' }
-    go ty@(LitTy {})   = return ty
-    go (CastTy ty co)  = mkCastTy <$> go ty <*> mapCoercion mapper env co
-    go (CoercionTy co) = CoercionTy <$> mapCoercion mapper env co
 
 {-# INLINABLE mapCoercion #-}  -- See Note [Specialising mappers]
 mapCoercion :: Monad m
@@ -746,7 +752,7 @@ splitAppTy_maybe ty = repSplitAppTy_maybe ty
 repSplitAppTy_maybe :: HasDebugCallStack => Type -> Maybe (Type,Type)
 -- ^ Does the AppTy split as in 'splitAppTy_maybe', but assumes that
 -- any Core view stuff is already done
-repSplitAppTy_maybe (FunTy ty1 ty2)
+repSplitAppTy_maybe (FunTy ty1 ty2)
   = Just (TyConApp funTyCon [rep1, rep2, ty1], ty2)
   where
     rep1 = getRuntimeRep ty1
@@ -768,10 +774,8 @@ repSplitAppTy_maybe _other = Nothing
 tcRepSplitAppTy_maybe :: Type -> Maybe (Type,Type)
 -- ^ Does the AppTy split as in 'tcSplitAppTy_maybe', but assumes that
 -- any coreView stuff is already done. Refuses to look through (c => t)
--- The "Rep" means that we assumes that any tcView stuff is already done.
--- Refuses to look through (c => t)
-tcRepSplitAppTy_maybe (FunTy ty1 ty2)
-  | isPredTy ty1
+tcRepSplitAppTy_maybe (FunTy { ft_af = af, ft_arg = ty1, ft_res = ty2 })
+  | InvisArg <- af
   = Nothing  -- See Note [Decomposing fat arrow c=>t]
 
   | otherwise
@@ -787,31 +791,6 @@ tcRepSplitAppTy_maybe (TyConApp tc tys)
   = Just (TyConApp tc tys', ty')    -- Never create unsaturated type family apps!
 tcRepSplitAppTy_maybe _other = Nothing
 
--- | Like 'tcSplitTyConApp_maybe' but doesn't look through type synonyms.
-tcRepSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
--- The "Rep" means that we assumes that any tcView stuff is already done.
--- Defined here to avoid module loops between Unify and TcType.
-tcRepSplitTyConApp_maybe (TyConApp tc tys)
-  = Just (tc, tys)
-
-tcRepSplitTyConApp_maybe (FunTy arg res)
-  = Just (funTyCon, [arg_rep, res_rep, arg, res])
-  where
-    arg_rep = getRuntimeRep arg
-    res_rep = getRuntimeRep res
-
-tcRepSplitTyConApp_maybe _
-  = Nothing
-
--- | Like 'tcSplitTyConApp' but doesn't look through type synonyms.
-tcRepSplitTyConApp :: HasCallStack => Type -> (TyCon, [Type])
--- The "Rep" means that we assumes that any tcView stuff is already done.
--- Defined here to avoid module loops between Unify and TcType.
-tcRepSplitTyConApp ty =
-  case tcRepSplitTyConApp_maybe ty of
-    Just stuff -> stuff
-    Nothing    -> pprPanic "tcRepSplitTyConApp" (ppr ty)
-
 -------------
 splitAppTy :: Type -> (Type, Type)
 -- ^ Attempts to take a type application apart, as in 'splitAppTy_maybe',
@@ -836,7 +815,7 @@ splitAppTys ty = split ty ty []
             (tc_args1, tc_args2) = splitAt n tc_args
         in
         (TyConApp tc tc_args1, tc_args2 ++ args)
-    split _   (FunTy ty1 ty2) args
+    split _   (FunTy ty1 ty2) args
       = ASSERT( null args )
         (TyConApp funTyCon [], [rep1, rep2, ty1, ty2])
       where
@@ -856,7 +835,7 @@ repSplitAppTys ty = split ty []
             (tc_args1, tc_args2) = splitAt n tc_args
         in
         (TyConApp tc tc_args1, tc_args2 ++ args)
-    split (FunTy ty1 ty2) args
+    split (FunTy ty1 ty2) args
       = ASSERT( null args )
         (TyConApp funTyCon [], [rep1, rep2, ty1, ty2])
       where
@@ -973,33 +952,33 @@ splitFunTy :: Type -> (Type, Type)
 -- ^ Attempts to extract the argument and result types from a type, and
 -- panics if that is not possible. See also 'splitFunTy_maybe'
 splitFunTy ty | Just ty' <- coreView ty = splitFunTy ty'
-splitFunTy (FunTy arg res) = (arg, res)
-splitFunTy other           = pprPanic "splitFunTy" (ppr other)
+splitFunTy (FunTy arg res) = (arg, res)
+splitFunTy other             = pprPanic "splitFunTy" (ppr other)
 
 splitFunTy_maybe :: Type -> Maybe (Type, Type)
 -- ^ Attempts to extract the argument and result types from a type
 splitFunTy_maybe ty | Just ty' <- coreView ty = splitFunTy_maybe ty'
-splitFunTy_maybe (FunTy arg res) = Just (arg, res)
-splitFunTy_maybe _               = Nothing
+splitFunTy_maybe (FunTy arg res) = Just (arg, res)
+splitFunTy_maybe _                 = Nothing
 
 splitFunTys :: Type -> ([Type], Type)
 splitFunTys ty = split [] ty ty
   where
     split args orig_ty ty | Just ty' <- coreView ty = split args orig_ty ty'
-    split args _       (FunTy arg res) = split (arg:args) res res
-    split args orig_ty _               = (reverse args, orig_ty)
+    split args _       (FunTy arg res) = split (arg:args) res res
+    split args orig_ty _                 = (reverse args, orig_ty)
 
 funResultTy :: Type -> Type
 -- ^ Extract the function result type and panic if that is not possible
 funResultTy ty | Just ty' <- coreView ty = funResultTy ty'
-funResultTy (FunTy _ res) = res
-funResultTy ty            = pprPanic "funResultTy" (ppr ty)
+funResultTy (FunTy { ft_res = res }) = res
+funResultTy ty                       = pprPanic "funResultTy" (ppr ty)
 
 funArgTy :: Type -> Type
 -- ^ Extract the function argument type and panic if that is not possible
 funArgTy ty | Just ty' <- coreView ty = funArgTy ty'
-funArgTy (FunTy arg _res) = arg
-funArgTy ty               = pprPanic "funArgTy" (ppr ty)
+funArgTy (FunTy { ft_arg = arg })    = arg
+funArgTy ty                           = pprPanic "funArgTy" (ppr ty)
 
 -- ^ Just like 'piResultTys' but for a single argument
 -- Try not to iterate 'piResultTy', because it's inefficient to substitute
@@ -1015,7 +994,7 @@ piResultTy_maybe :: Type -> Type -> Maybe Type
 piResultTy_maybe ty arg
   | Just ty' <- coreView ty = piResultTy_maybe ty' arg
 
-  | FunTy _ res <- ty
+  | FunTy { ft_res = res } <- ty
   = Just res
 
   | ForAllTy (Bndr tv _) res <- ty
@@ -1053,7 +1032,7 @@ piResultTys ty orig_args@(arg:args)
   | Just ty' <- coreView ty
   = piResultTys ty' orig_args
 
-  | FunTy _ res <- ty
+  | FunTy { ft_res = res } <- ty
   = piResultTys res args
 
   | ForAllTy (Bndr tv _) res <- ty
@@ -1071,7 +1050,7 @@ piResultTys ty orig_args@(arg:args)
       | Just ty' <- coreView ty
       = go subst ty' all_args
 
-      | FunTy _ res <- ty
+      | FunTy { ft_res = res } <- ty
       = go subst res args
 
       | ForAllTy (Bndr tv _) res <- ty
@@ -1142,7 +1121,8 @@ mkTyConApp :: TyCon -> [Type] -> Type
 mkTyConApp tycon tys
   | isFunTyCon tycon
   , [_rep1,_rep2,ty1,ty2] <- tys
-  = FunTy ty1 ty2
+  = FunTy { ft_af = VisArg, ft_arg = ty1, ft_res = ty2 }
+    -- The FunTyCon (->) is always a visible one
 
   | otherwise
   = TyConApp tycon tys
@@ -1173,7 +1153,7 @@ tyConAppTyCon ty = tyConAppTyCon_maybe ty `orElse` pprPanic "tyConAppTyCon" (ppr
 tyConAppArgs_maybe :: Type -> Maybe [Type]
 tyConAppArgs_maybe ty | Just ty' <- coreView ty = tyConAppArgs_maybe ty'
 tyConAppArgs_maybe (TyConApp _ tys) = Just tys
-tyConAppArgs_maybe (FunTy arg res)
+tyConAppArgs_maybe (FunTy arg res)
   | Just rep1 <- getRuntimeRep_maybe arg
   , Just rep2 <- getRuntimeRep_maybe res
   = Just [rep1, rep2, arg, res]
@@ -1203,16 +1183,25 @@ splitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type])
 splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
 splitTyConApp_maybe ty                           = repSplitTyConApp_maybe ty
 
--- | Like 'splitTyConApp_maybe', but doesn't look through synonyms. This
--- assumes the synonyms have already been dealt with.
+-------------------
 repSplitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type])
+-- ^ Like 'splitTyConApp_maybe', but doesn't look through synonyms. This
+-- assumes the synonyms have already been dealt with.
+--
+-- Moreover, for a FunTy, it only succeeds if the argument types
+-- have enough info to extract the runtime-rep arguments that
+-- the funTyCon requires.  This will usually be true;
+-- but may be temporarily false during canonicalization:
+--     see Note [FunTy and decomposing tycon applications] in TcCanonical
+--
 repSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
-repSplitTyConApp_maybe (FunTy arg res)
+repSplitTyConApp_maybe (FunTy arg res)
   | Just arg_rep <- getRuntimeRep_maybe arg
   , Just res_rep <- getRuntimeRep_maybe res
   = Just (funTyCon, [arg_rep, res_rep, arg, res])
 repSplitTyConApp_maybe _ = Nothing
 
+-------------------
 -- | Attempts to tease a list type apart and gives the type of the elements if
 -- successful (looks through type synonyms)
 splitListTyConApp_maybe :: Type -> Maybe Type
@@ -1286,7 +1275,7 @@ tyConBindersTyCoBinders :: [TyConBinder] -> [TyCoBinder]
 tyConBindersTyCoBinders = map to_tyb
   where
     to_tyb (Bndr tv (NamedTCB vis)) = Named (Bndr tv vis)
-    to_tyb (Bndr tv AnonTCB)        = Anon (varType tv)
+    to_tyb (Bndr tv (AnonTCB af))   = Anon af (varType tv)
 
 {-
 --------------------------------------------------------------------
@@ -1341,7 +1330,7 @@ mkTyCoInvForAllTy :: TyCoVar -> Type -> Type
 mkTyCoInvForAllTy tv ty
   | isCoVar tv
   , not (tv `elemVarSet` tyCoVarsOfType ty)
-  = mkFunTy (varType tv) ty
+  = mkVisFunTy (varType tv) ty
   | otherwise
   = ForAllTy (Bndr tv Inferred) ty
 
@@ -1385,17 +1374,52 @@ mkLamType  :: Var -> Type -> Type
 mkLamTypes :: [Var] -> Type -> Type
 -- ^ 'mkLamType' for multiple type or value arguments
 
-mkLamType v ty
-   | isCoVar v
-   , v `elemVarSet` tyCoVarsOfType ty
-   = ForAllTy (Bndr v Inferred) ty
+mkLamType v body_ty
    | isTyVar v
-   = ForAllTy (Bndr v Inferred) ty
+   = ForAllTy (Bndr v Inferred) body_ty
+
+   | isCoVar v
+   , v `elemVarSet` tyCoVarsOfType body_ty
+   = ForAllTy (Bndr v Required) body_ty
+
+   | isPredTy arg_ty  -- See Note [mkLamType: dictionary arguments]
+   = mkInvisFunTy arg_ty body_ty
+
    | otherwise
-   = FunTy (varType v) ty
+   = mkVisFunTy arg_ty body_ty
+   where
+     arg_ty = varType v
 
 mkLamTypes vs ty = foldr mkLamType ty vs
 
+{- Note [mkLamType: dictionary arguments]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If we have (\ (d :: Ord a). blah), we want to give it type
+           (Ord a => blah_ty)
+with a fat arrow; that is, using mkInvisFunTy, not mkVisFunTy.
+
+Why? After all, we are in Core, where (=>) and (->) behave the same.
+Yes, but the /specialiser/ does treat dictionary arguments specially.
+Suppose we do w/w on 'foo' in module A, thus (Trac #11272, #6056)
+   foo :: Ord a => Int -> blah
+   foo a d x = case x of I# x' -> $wfoo @a d x'
+
+   $wfoo :: Ord a => Int# -> blah
+
+Now in module B we see (foo @Int dOrdInt).  The specialiser will
+specialise this to $sfoo, where
+   $sfoo :: Int -> blah
+   $sfoo x = case x of I# x' -> $wfoo @Int dOrdInt x'
+
+Now we /must/ also specialise $wfoo!  But it wasn't user-written,
+and has a type built with mkLamTypes.
+
+Conclusion: the easiest thing is to make mkLamType build
+            (c => ty)
+when the argument is a predicate type.  See TyCoRep
+Note [Types for coercions, predicates, and evidence]
+-}
+
 -- | Given a list of type-level vars and the free vars of a result kind,
 -- makes TyCoBinders, preferring anonymous binders
 -- if the variable is, in fact, not dependent.
@@ -1415,7 +1439,7 @@ mkTyConBindersPreferAnon vars inner_tkvs = ASSERT( all isTyVar vars)
               = ( Bndr v (NamedTCB Required) : binders
                 , fvs `delVarSet` v `unionVarSet` kind_vars )
               | otherwise
-              = ( Bndr v AnonTCB : binders
+              = ( Bndr v (AnonTCB VisArg) : binders
                 , fvs `unionVarSet` kind_vars )
       where
         (binders, fvs) = go vs
@@ -1518,7 +1542,8 @@ splitPiTy_maybe ty = go ty
   where
     go ty | Just ty' <- coreView ty = go ty'
     go (ForAllTy bndr ty) = Just (Named bndr, ty)
-    go (FunTy arg res)    = Just (Anon arg, res)
+    go (FunTy { ft_af = af, ft_arg = arg, ft_res = res})
+                          = Just (Anon af arg, res)
     go _                  = Nothing
 
 -- | Takes a forall type apart, or panics
@@ -1534,7 +1559,8 @@ splitPiTys ty = split ty ty []
   where
     split orig_ty ty bs | Just ty' <- coreView ty = split orig_ty ty' bs
     split _       (ForAllTy b res) bs = split res res (Named b  : bs)
-    split _       (FunTy arg res)  bs = split res res (Anon arg : bs)
+    split _       (FunTy { ft_af = af, ft_arg = arg, ft_res = res }) bs
+                                      = split res res (Anon af arg : bs)
     split orig_ty _                bs = (reverse bs, orig_ty)
 
 -- | Like 'splitPiTys' but split off only /named/ binders
@@ -1564,8 +1590,8 @@ splitPiTysInvisible ty = split ty ty []
     split _ (ForAllTy b res) bs
       | Bndr _ vis <- b
       , isInvisibleArgFlag vis   = split res res (Named b  : bs)
-    split _ (FunTy arg res)  bs
-      | isPredTy arg             = split res res (Anon arg : bs)
+    split _ (FunTy { ft_af = InvisArg, ft_arg = arg, ft_res = res })  bs
+                                 = split res res (Anon InvisArg arg : bs)
     split orig_ty _          bs  = (reverse bs, orig_ty)
 
 splitPiTysInvisibleN :: Int -> Type -> ([TyCoBinder], Type)
@@ -1580,8 +1606,8 @@ splitPiTysInvisibleN n ty = split n ty ty []
       | ForAllTy b res <- ty
       , Bndr _ vis <- b
       , isInvisibleArgFlag vis  = split (n-1) res res (Named b  : bs)
-      | FunTy arg res <- ty
-      , isPredTy arg            = split (n-1) res res (Anon arg : bs)
+      | FunTy { ft_af = InvisArg, ft_arg = arg, ft_res = res } <- ty
+                                = split (n-1) res res (Anon InvisArg arg : bs)
       | otherwise               = (reverse bs, orig_ty)
 
 -- | Given a 'TyCon' and a list of argument types, filter out any invisible
@@ -1671,7 +1697,7 @@ isTauTy (TyVarTy _)           = True
 isTauTy (LitTy {})            = True
 isTauTy (TyConApp tc tys)     = all isTauTy tys && isTauTyCon tc
 isTauTy (AppTy a b)           = isTauTy a && isTauTy b
-isTauTy (FunTy a b)           = isTauTy a && isTauTy b
+isTauTy (FunTy _ a b)         = isTauTy a && isTauTy b
 isTauTy (ForAllTy {})         = False
 isTauTy (CastTy ty _)         = isTauTy ty
 isTauTy (CoercionTy _)        = False  -- Not sure about this
@@ -1685,7 +1711,7 @@ isTauTy (CoercionTy _)        = False  -- Not sure about this
 -}
 
 -- | Make an anonymous binder
-mkAnonBinder :: Type -> TyCoBinder
+mkAnonBinder :: AnonArgFlag -> Type -> TyCoBinder
 mkAnonBinder = Anon
 
 -- | Does this binder bind a variable that is /not/ erased? Returns
@@ -1701,27 +1727,18 @@ tyCoBinderVar_maybe _          = Nothing
 tyCoBinderType :: TyCoBinder -> Type
 -- Barely used
 tyCoBinderType (Named tvb) = binderType tvb
-tyCoBinderType (Anon ty)   = ty
+tyCoBinderType (Anon _ ty) = ty
 
 tyBinderType :: TyBinder -> Type
 tyBinderType (Named (Bndr tv _))
   = ASSERT( isTyVar tv )
     tyVarKind tv
-tyBinderType (Anon ty)   = ty
+tyBinderType (Anon ty)   = ty
 
 -- | Extract a relevant type, if there is one.
 binderRelevantType_maybe :: TyCoBinder -> Maybe Type
-binderRelevantType_maybe (Named {}) = Nothing
-binderRelevantType_maybe (Anon ty)  = Just ty
-
--- | Like 'maybe', but for binders.
-caseBinder :: TyCoBinder           -- ^ binder to scrutinize
-           -> (TyCoVarBinder -> a) -- ^ named case
-           -> (Type -> a)          -- ^ anonymous case
-           -> a
-caseBinder (Named v) f _ = f v
-caseBinder (Anon t)  _ d = d t
-
+binderRelevantType_maybe (Named {})  = Nothing
+binderRelevantType_maybe (Anon _ ty) = Just ty
 
 {-
 %************************************************************************
@@ -1732,36 +1749,6 @@ caseBinder (Anon t)  _ d = d t
 
 Predicates on PredType
 
-Note [Types for coercions, predicates, and evidence]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We treat differently:
-
-  (a) Predicate types
-        Test: isPredTy
-        Binders: DictIds
-        Kind: Constraint
-        Examples: (Eq a), and (a ~ b)
-
-  (b) Coercion types are primitive, unboxed equalities
-        Test: isCoVarTy
-        Binders: CoVars (can appear in coercions)
-        Kind: TYPE (TupleRep [])
-        Examples: (t1 ~# t2) or (t1 ~R# t2)
-
-  (c) Evidence types is the type of evidence manipulated by
-      the type constraint solver.
-        Test: isEvVarType
-        Binders: EvVars
-        Kind: Constraint or TYPE (TupleRep [])
-        Examples: all coercion types and predicate types
-
-Coercion types and predicate types are mutually exclusive,
-but evidence types are a superset of both.
-
-When treated as a user type, predicates are invisible and are
-implicitly instantiated; but coercion types, and non-pred evidence
-types, are just regular old types.
-
 Note [Evidence for quantified constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The superclass mechanism in TcCanonical.makeSuperClasses risks
@@ -1786,7 +1773,7 @@ in TcCanonical.
 tcSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
 -- Defined here to avoid module loops between Unify and TcType.
 tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
-tcSplitTyConApp_maybe ty                         = tcRepSplitTyConApp_maybe ty
+tcSplitTyConApp_maybe ty                         = repSplitTyConApp_maybe ty
 
 -- tcIsConstraintKind stuf only makes sense in the typechecker
 -- After that Constraint = Type
@@ -1819,10 +1806,10 @@ tcReturnsConstraintKind :: Kind -> Bool
 --         forall k. k -> Constraint
 tcReturnsConstraintKind kind
   | Just kind' <- tcView kind = tcReturnsConstraintKind kind'
-tcReturnsConstraintKind (ForAllTy _ ty) = tcReturnsConstraintKind ty
-tcReturnsConstraintKind (FunTy    _ ty) = tcReturnsConstraintKind ty
-tcReturnsConstraintKind (TyConApp tc _) = isConstraintKindCon tc
-tcReturnsConstraintKind _               = False
+tcReturnsConstraintKind (ForAllTy _ ty)         = tcReturnsConstraintKind ty
+tcReturnsConstraintKind (FunTy { ft_res = ty }) = tcReturnsConstraintKind ty
+tcReturnsConstraintKind (TyConApp tc _)         = isConstraintKindCon tc
+tcReturnsConstraintKind _                       = False
 
 isEvVarType :: Type -> Bool
 -- True of (a) predicates, of kind Constraint, such as (Eq a), and (a ~ b)
@@ -1836,25 +1823,32 @@ isEvVarType ty = isCoVarType ty || isPredTy ty
 --    (t1 ~# t2) or (t1 ~R# t2)
 -- See Note [Types for coercions, predicates, and evidence]
 isCoVarType :: Type -> Bool
-isCoVarType ty
-  | Just (tc,tys) <- splitTyConApp_maybe ty
-  , (tc `hasKey` eqPrimTyConKey) || (tc `hasKey` eqReprPrimTyConKey)
-  , tys `lengthIs` 4
-  = True
-isCoVarType _ = False
-
-isClassPred, isEqPred, isNomEqPred, isIPPred :: PredType -> Bool
+isCoVarType ty = isEqPrimPred ty
+
+isEqPredClass :: Class -> Bool
+-- True of (~) and (~~)
+isEqPredClass cls =  cls `hasKey` eqTyConKey
+                  || cls `hasKey` heqTyConKey
+
+isClassPred, isEqPred, isEqPrimPred, isIPPred :: PredType -> Bool
 isClassPred ty = case tyConAppTyCon_maybe ty of
     Just tyCon | isClassTyCon tyCon -> True
     _                               -> False
-isEqPred ty = case tyConAppTyCon_maybe ty of
-    Just tyCon -> tyCon `hasKey` eqPrimTyConKey
-               || tyCon `hasKey` eqReprPrimTyConKey
-    _          -> False
 
-isNomEqPred ty = case tyConAppTyCon_maybe ty of
-    Just tyCon -> tyCon `hasKey` eqPrimTyConKey
-    _          -> False
+isEqPred ty  -- True of (a ~ b) and (a ~~ b)
+             -- ToDo: should we check saturation?
+  | Just tc <- tyConAppTyCon_maybe ty
+  , Just cls <- tyConClass_maybe tc
+  = isEqPredClass cls
+  | otherwise
+  = False
+
+isEqPrimPred ty  -- True of (a ~# b) (a ~R# b)
+             -- ToDo: should we check saturation?
+  | Just tc <- tyConAppTyCon_maybe ty
+  = tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
+  | otherwise
+  = False
 
 isIPPred ty = case tyConAppTyCon_maybe ty of
     Just tc -> isIPTyCon tc
@@ -1943,9 +1937,8 @@ isDictLikeTy ty = case splitTyConApp_maybe ty of
                        | isTupleTyCon tc -> all isDictLikeTy tys
         _other                           -> False
 
-{-
-Note [Dictionary-like types]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Dictionary-like types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Being "dictionary-like" means either a dictionary type or a tuple thereof.
 In GHC 6.10 we build implication constraints which construct such tuples,
 and if we land up with a binding
@@ -1973,8 +1966,7 @@ we ended up with something like
 This is all a bit ad-hoc; eg it relies on knowing that implication
 constraints build tuples.
 
-
-Decomposing PredType
+ToDo: it would be far easier just to use isPredTy.
 -}
 
 -- | A choice of equality relation. This is separate from the type 'Role'
@@ -2253,7 +2245,7 @@ isFamFreeTy (TyVarTy _)       = True
 isFamFreeTy (LitTy {})        = True
 isFamFreeTy (TyConApp tc tys) = all isFamFreeTy tys && isFamFreeTyCon tc
 isFamFreeTy (AppTy a b)       = isFamFreeTy a && isFamFreeTy b
-isFamFreeTy (FunTy a b)       = isFamFreeTy a && isFamFreeTy b
+isFamFreeTy (FunTy _ a b)     = isFamFreeTy a && isFamFreeTy b
 isFamFreeTy (ForAllTy _ ty)   = isFamFreeTy ty
 isFamFreeTy (CastTy ty _)     = isFamFreeTy ty
 isFamFreeTy (CoercionTy _)    = False  -- Not sure about this
@@ -2439,7 +2431,7 @@ seqType :: Type -> ()
 seqType (LitTy n)                   = n `seq` ()
 seqType (TyVarTy tv)                = tv `seq` ()
 seqType (AppTy t1 t2)               = seqType t1 `seq` seqType t2
-seqType (FunTy t1 t2)               = seqType t1 `seq` seqType t2
+seqType (FunTy _ t1 t2)             = seqType t1 `seq` seqType t2
 seqType (TyConApp tc tys)           = tc `seq` seqTypes tys
 seqType (ForAllTy (Bndr tv _) ty)   = seqType (varType tv) `seq` seqType ty
 seqType (CastTy ty co)              = seqType ty `seq` seqCo co
@@ -2592,7 +2584,7 @@ nonDetCmpTypeX env orig_t1 orig_t2 =
     go env ty1 (AppTy s2 t2)
       | Just (s1, t1) <- repSplitAppTy_maybe ty1
       = go env s1 s2 `thenCmpTy` go env t1 t2
-    go env (FunTy s1 t1) (FunTy s2 t2)
+    go env (FunTy _ s1 t1) (FunTy _ s2 t2)
       = go env s1 s2 `thenCmpTy` go env t1 t2
     go env (TyConApp tc1 tys1) (TyConApp tc2 tys2)
       = liftOrdering (tc1 `nonDetCmpTc` tc2) `thenCmpTy` gos env tys1 tys2
@@ -2747,9 +2739,12 @@ tcTypeKind (TyVarTy tyvar)   = tyVarKind tyvar
 tcTypeKind (CastTy _ty co)   = pSnd $ coercionKind co
 tcTypeKind (CoercionTy co)   = coercionType co
 
-tcTypeKind (FunTy arg res)
-  | isPredTy arg, isPredTy res = constraintKind
-  | otherwise                  = liftedTypeKind
+tcTypeKind (FunTy { ft_af = af, ft_res = res })
+  | InvisArg <- af
+  , tcIsConstraintKind (tcTypeKind res)
+  = constraintKind     -- Eq a => Ord a         :: Constraint
+  | otherwise          -- Eq a => a -> a        :: TYPE LiftedRep
+  = liftedTypeKind     -- Eq a => Array# Int    :: Type LiftedRep (not TYPE PtrRep)
 
 tcTypeKind (AppTy fun arg)
   = go fun [arg]
@@ -2861,9 +2856,10 @@ occCheckExpand vs_to_avoid ty
     go cxt (AppTy ty1 ty2) = do { ty1' <- go cxt ty1
                                 ; ty2' <- go cxt ty2
                                 ; return (mkAppTy ty1' ty2') }
-    go cxt (FunTy ty1 ty2) = do { ty1' <- go cxt ty1
-                                ; ty2' <- go cxt ty2
-                                ; return (mkFunTy ty1' ty2') }
+    go cxt ty@(FunTy _ ty1 ty2)
+       = do { ty1' <- go cxt ty1
+            ; ty2' <- go cxt ty2
+            ; return (ty { ft_arg = ty1', ft_res = ty2' }) }
     go cxt@(as, env) (ForAllTy (Bndr tv vis) body_ty)
        = do { ki' <- go cxt (varType tv)
             ; let tv' = setVarType tv ki'
@@ -2982,7 +2978,7 @@ tyConsOfType ty
      go (LitTy {})                  = emptyUniqSet
      go (TyConApp tc tys)           = go_tc tc `unionUniqSets` go_s tys
      go (AppTy a b)                 = go a `unionUniqSets` go b
-     go (FunTy a b)                 = go a `unionUniqSets` go b `unionUniqSets` go_tc funTyCon
+     go (FunTy _ a b)               = go a `unionUniqSets` go b `unionUniqSets` go_tc funTyCon
      go (ForAllTy (Bndr tv _) ty)   = go ty `unionUniqSets` go (varType tv)
      go (CastTy ty co)              = go ty `unionUniqSets` go_co co
      go (CoercionTy co)             = go_co co
@@ -3041,7 +3037,7 @@ splitVisVarsOfType orig_ty = Pair invis_vars vis_vars
     go (TyVarTy tv)      = Pair (tyCoVarsOfType $ tyVarKind tv) (unitVarSet tv)
     go (AppTy t1 t2)     = go t1 `mappend` go t2
     go (TyConApp tc tys) = go_tc tc tys
-    go (FunTy t1 t2)     = go t1 `mappend` go t2
+    go (FunTy _ t1 t2)   = go t1 `mappend` go t2
     go (ForAllTy (Bndr tv _) ty)
       = ((`delVarSet` tv) <$> go ty) `mappend`
         (invisible (tyCoVarsOfType $ varType tv))
@@ -3068,7 +3064,7 @@ modifyJoinResTy orig_ar f orig_ty
   where
     go 0 ty = f ty
     go n ty | Just (arg_bndr, res_ty) <- splitPiTy_maybe ty
-            = mkTyCoPiTy arg_bndr (go (n-1) res_ty)
+            = mkPiTy arg_bndr (go (n-1) res_ty)
             | otherwise
             = pprPanic "modifyJoinResTy" (ppr orig_ar <+> ppr orig_ty)
 
index d132666..9720afc 100644 (file)
@@ -1438,7 +1438,7 @@ ty_co_match menv subst ty1 (AppCo co2 arg2) _lkco _rkco
 
 ty_co_match menv subst (TyConApp tc1 tys) (TyConAppCo _ tc2 cos) _lkco _rkco
   = ty_co_match_tc menv subst tc1 tys tc2 cos
-ty_co_match menv subst (FunTy ty1 ty2) co _lkco _rkco
+ty_co_match menv subst (FunTy ty1 ty2) co _lkco _rkco
     -- Despite the fact that (->) is polymorphic in four type variables (two
     -- runtime rep and two types), we shouldn't need to explicitly unify the
     -- runtime reps here; unifying the types themselves should be sufficient.
@@ -1550,7 +1550,7 @@ pushRefl co =
   case (isReflCo_maybe co) of
     Just (AppTy ty1 ty2, Nominal)
       -> Just (AppCo (mkReflCo Nominal ty1) (mkNomReflCo ty2))
-    Just (FunTy ty1 ty2, r)
+    Just (FunTy ty1 ty2, r)
       | Just rep1 <- getRuntimeRep_maybe ty1
       , Just rep2 <- getRuntimeRep_maybe ty2
       ->  Just (TyConAppCo r funTyCon [ mkReflCo r rep1, mkReflCo r rep2
index c3090b0..3880cb9 100644 (file)
@@ -9276,6 +9276,28 @@ distinction). GHC does not consider ``forall k. k -> Type`` and
 ``forall {k}. k -> Type`` to be equal at the kind level, and thus rejects
 ``Foo Proxy`` as ill-kinded.
 
+Constraints in kinds
+--------------------
+
+As kinds and types are the same, kinds can (with :extension:`TypeInType`)
+contain type constraints. However, only equality constraints are supported.
+
+Here is an example of a constrained kind: ::
+
+  type family IsTypeLit a where
+    IsTypeLit Nat    = 'True
+    IsTypeLit Symbol = 'True
+    IsTypeLit a      = 'False
+
+  data T :: forall a. (IsTypeLit a ~ 'True) => a -> Type where
+    MkNat    :: T 42
+    MkSymbol :: T "Don't panic!"
+
+The declarations above are accepted. However, if we add ``MkOther :: T Int``,
+we get an error that the equality constraint is not satisfied; ``Int`` is
+not a type literal. Note that explicitly quantifying with ``forall a`` is
+not necessary here.
+
 The kind ``Type``
 -----------------
 
index 1100ff6..00583d0 100644 (file)
@@ -27,16 +27,16 @@ import FastString
 go, go2, x, d, n, y, z, scrutf, scruta :: Id
 [go, go2, x,d, n, y, z, scrutf, scruta, f] = mkTestIds
     (words "go go2 x d n y z scrutf scruta f")
-    [ mkFunTys [intTy, intTy] intTy
-    , mkFunTys [intTy, intTy] intTy
+    [ mkVisFunTys [intTy, intTy] intTy
+    , mkVisFunTys [intTy, intTy] intTy
     , intTy
-    , mkFunTys [intTy] intTy
-    , mkFunTys [intTy] intTy
+    , mkVisFunTys [intTy] intTy
+    , mkVisFunTys [intTy] intTy
     , intTy
     , intTy
-    , mkFunTys [boolTy] boolTy
+    , mkVisFunTys [boolTy] boolTy
     , boolTy
-    , mkFunTys [intTy, intTy] intTy -- protoypical external function
+    , mkVisFunTys [intTy, intTy] intTy -- protoypical external function
     ]
 
 exprs :: [(String, CoreExpr)]
index 96fe043..e4968a1 100644 (file)
@@ -8,5 +8,9 @@ import Data.Kind
 data A :: Type -> Type where
   MkA :: Show (Maybe a) => A a
 
+data B :: Type -> Type where
+  MkB :: Show a => B a
+
 data SA :: forall a. A a -> Type where
   SMkA :: SA MkA
+  SMkB :: SA MkB
index 53aff76..be2d7c7 100644 (file)
@@ -5,8 +5,9 @@ T15215.hs:9:3: error:
     • In the definition of data constructor ‘MkA’
       In the data type declaration for ‘A’
 
-T15215.hs:12:14: error:
-    • Illegal constraint in a kind: Show (Maybe a0)
-    • In the first argument of ‘SA’, namely ‘MkA’
-      In the type ‘SA MkA’
-      In the definition of data constructor ‘SMkA’
+T15215.hs:16:14: error:
+    • Data constructor ‘MkB’ cannot be used here
+        (it has an unpromotable context ‘Show a’)
+    • In the first argument of ‘SA’, namely ‘MkB’
+      In the type ‘SA MkB’
+      In the definition of data constructor ‘SMkB’
index 9c34ed4..8a885b3 100644 (file)
@@ -206,4 +206,3 @@ test('T14887a', normal, compile, [''])
 test('T14847', normal, compile, [''])
 test('T15795', normal, compile, [''])
 test('T15795a', normal, compile, [''])
-
index 6d21fef..b17c993 100644 (file)
@@ -1,7 +1,8 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeInType #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
+
 module T12102 where
 
 import Data.Kind
diff --git a/testsuite/tests/typecheck/should_fail/T12102.stderr b/testsuite/tests/typecheck/should_fail/T12102.stderr
deleted file mode 100644 (file)
index ea3016b..0000000
+++ /dev/null
@@ -1,6 +0,0 @@
-
-T12102.hs:15:1: error:
-    • Illegal constraint in a kind: forall a.
-                                    (IsTypeLit a ~ 'True) =>
-                                    a -> *
-    • In the data type declaration for ‘T’
index bb7ed96..1a775d3 100644 (file)
@@ -409,7 +409,7 @@ test('T12063', [expect_broken(12063)], multimod_compile_fail, ['T12063', '-v0'])
 test('T12083a', normal, compile_fail, [''])
 test('T12083b', normal, compile_fail, [''])
 test('T11974b', normal, compile_fail, [''])
-test('T12102', normal, compile_fail, [''])
+test('T12102', normal, compile, [''])
 test('T12151', normal, compile_fail, [''])
 test('T7437', normal, compile_fail, [''])
 test('T12177', normal, compile_fail, [''])
index 863a7d2..d7ae9ff 100644 (file)
@@ -890,8 +890,8 @@ ppType (TyApp (VecTyCon _ pptc) [])      = pptc
 ppType (TyUTup ts) = "(mkTupleTy Unboxed "
                      ++ listify (map ppType ts) ++ ")"
 
-ppType (TyF s d) = "(mkFunTy (" ++ ppType s ++ ") (" ++ ppType d ++ "))"
-ppType (TyC s d) = "(mkFunTy (" ++ ppType s ++ ") (" ++ ppType d ++ "))"
+ppType (TyF s d) = "(mkVisFunTy (" ++ ppType s ++ ") (" ++ ppType d ++ "))"
+ppType (TyC s d) = "(mkInvisFunTy (" ++ ppType s ++ ") (" ++ ppType d ++ "))"
 
 ppType other
    = error ("ppType: can't handle: " ++ show other ++ "\n")
index 1a4715b..c323c25 160000 (submodule)
@@ -1 +1 @@
-Subproject commit 1a4715b2c14d6387da91e74560845fb6cbe6808b
+Subproject commit c323c257be0bc118a0501416f06bda8fd51c92f9