diff options
| author | Simon Peyton Jones <simonpj@microsoft.com> | 2019-02-15 09:53:48 +0000 |
|---|---|---|
| committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2019-02-23 21:31:47 -0500 |
| commit | 6cce36f83aec33d33545e0ef2135894d22dff5ca (patch) | |
| tree | 3bfa83e7ba313f7a10b9219cb58eb18a8d368b2d | |
| parent | ac34e784775a0fa8b7284d42ff89571907afdc36 (diff) | |
| download | haskell-6cce36f83aec33d33545e0ef2135894d22dff5ca.tar.gz | |
Add AnonArgFlag to FunTy
The big payload of this patch is:
Add an AnonArgFlag to the FunTy constructor
of Type, so that
(FunTy VisArg t1 t2) means (t1 -> t2)
(FunTy InvisArg t1 t2) means (t1 => t2)
The big payoff is that we have a simple, local test to make
when decomposing a type, leading to many fewer calls to
isPredTy. To me the code seems a lot tidier, and probably
more efficient (isPredTy has to take the kind of the type).
See Note [Function types] in TyCoRep.
There are lots of consequences
* I made FunTy into a record, so that it'll be easier
when we add a linearity field, something that is coming
down the road.
* Lots of code gets touched in a routine way, simply because it
pattern matches on FunTy.
* I wanted to make a pattern synonym for (FunTy2 arg res), which
picks out just the argument and result type from the record. But
alas the pattern-match overlap checker has a heart attack, and
either reports false positives, or takes too long. In the end
I gave up on pattern synonyms.
There's some commented-out code in TyCoRep that shows what I
wanted to do.
* Much more clarity about predicate types, constraint types
and (in particular) equality constraints in kinds. See TyCoRep
Note [Types for coercions, predicates, and evidence]
and Note [Constraints in kinds].
This made me realise that we need an AnonArgFlag on
AnonTCB in a TyConBinder, something that was really plain
wrong before. See TyCon Note [AnonTCB InivsArg]
* When building function types we must know whether we
need VisArg (mkVisFunTy) or InvisArg (mkInvisFunTy).
This turned out to be pretty easy in practice.
* Pretty-printing of types, esp in IfaceType, gets
tidier, because we were already recording the (->)
vs (=>) distinction in an ad-hoc way. Death to
IfaceFunTy.
* mkLamType needs to keep track of whether it is building
(t1 -> t2) or (t1 => t2). See Type
Note [mkLamType: dictionary arguments]
Other minor stuff
* Some tidy-up in validity checking involving constraints;
Trac #16263
83 files changed, 1045 insertions, 879 deletions
diff --git a/compiler/backpack/RnModIface.hs b/compiler/backpack/RnModIface.hs index 01cf47f039..af24fcced7 100644 --- a/compiler/backpack/RnModIface.hs +++ b/compiler/backpack/RnModIface.hs @@ -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) diff --git a/compiler/basicTypes/DataCon.hs b/compiler/basicTypes/DataCon.hs index f34a6cb74d..8baf43c7d3 100644 --- a/compiler/basicTypes/DataCon.hs +++ b/compiler/basicTypes/DataCon.hs @@ -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 diff --git a/compiler/basicTypes/MkId.hs b/compiler/basicTypes/MkId.hs index 1802cd769e..ceda50295c 100644 --- a/compiler/basicTypes/MkId.hs +++ b/compiler/basicTypes/MkId.hs @@ -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] $ diff --git a/compiler/basicTypes/PatSyn.hs b/compiler/basicTypes/PatSyn.hs index bf9426ecc8..2f8cee4149 100644 --- a/compiler/basicTypes/PatSyn.hs +++ b/compiler/basicTypes/PatSyn.hs @@ -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) diff --git a/compiler/basicTypes/Var.hs b/compiler/basicTypes/Var.hs index bfa5e5fa7a..7e451e5407 100644 --- a/compiler/basicTypes/Var.hs +++ b/compiler/basicTypes/Var.hs @@ -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 index 0000000000..aa022eaf27 --- /dev/null +++ b/compiler/basicTypes/Var.hs-boot @@ -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 diff --git a/compiler/codeGen/StgCmmClosure.hs b/compiler/codeGen/StgCmmClosure.hs index 8ad8951a21..8a32a7fff9 100644 --- a/compiler/codeGen/StgCmmClosure.hs +++ b/compiler/codeGen/StgCmmClosure.hs @@ -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 = diff --git a/compiler/coreSyn/CoreFVs.hs b/compiler/coreSyn/CoreFVs.hs index bc54d26ad3..18e109a745 100644 --- a/compiler/coreSyn/CoreFVs.hs +++ b/compiler/coreSyn/CoreFVs.hs @@ -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 diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs index 53cddbfabe..62ddb9f410 100644 --- a/compiler/coreSyn/CoreLint.hs +++ b/compiler/coreSyn/CoreLint.hs @@ -1349,7 +1349,7 @@ lintType ty@(TyConApp tc tys) -- arrows can related *unlifted* kinds, so this has to be separate from -- a dependent forall. -lintType ty@(FunTy t1 t2) +lintType ty@(FunTy _ t1 t2) = do { k1 <- lintType t1 ; k2 <- lintType t2 ; lintArrow (text "type or kind" <+> quotes (ppr ty)) k1 k2 } @@ -1509,7 +1509,7 @@ lint_app doc kfn kas | Just kfn' <- coreView kfn = go_app in_scope kfn' tka - go_app _ (FunTy kfa kfb) tka@(_,ka) + go_app _ (FunTy _ kfa kfb) tka@(_,ka) = do { unless (ka `eqType` kfa) $ addErrL (fail_msg (text "Fun:" <+> (ppr kfa $$ ppr tka))) ; return kfb } @@ -1765,7 +1765,7 @@ lintCoercion co@(FunCo r co1 co2) ; k' <- lintArrow (text "coercion" <+> quotes (ppr co)) k'1 k'2 ; lintRole co1 r r1 ; lintRole co2 r r2 - ; return (k, k', mkFunTy s1 s2, mkFunTy t1 t2, r) } + ; return (k, k', mkVisFunTy s1 s2, mkVisFunTy t1 t2, r) } lintCoercion (CoVarCo cv) | not (isCoVar cv) diff --git a/compiler/coreSyn/CoreMap.hs b/compiler/coreSyn/CoreMap.hs index 11f2fb1b11..3d0693466a 100644 --- a/compiler/coreSyn/CoreMap.hs +++ b/compiler/coreSyn/CoreMap.hs @@ -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' diff --git a/compiler/coreSyn/CoreUtils.hs b/compiler/coreSyn/CoreUtils.hs index 4602dfa065..ee79a0f930 100644 --- a/compiler/coreSyn/CoreUtils.hs +++ b/compiler/coreSyn/CoreUtils.hs @@ -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] diff --git a/compiler/coreSyn/MkCore.hs b/compiler/coreSyn/MkCore.hs index 1583c59148..999cfc7db5 100644 --- a/compiler/coreSyn/MkCore.hs +++ b/compiler/coreSyn/MkCore.hs @@ -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 diff --git a/compiler/deSugar/DsCCall.hs b/compiler/deSugar/DsCCall.hs index 7cab8e8e25..3df8ee11e0 100644 --- a/compiler/deSugar/DsCCall.hs +++ b/compiler/deSugar/DsCCall.hs @@ -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" diff --git a/compiler/deSugar/DsForeign.hs b/compiler/deSugar/DsForeign.hs index d34c3a791a..95a5e4af14 100644 --- a/compiler/deSugar/DsForeign.hs +++ b/compiler/deSugar/DsForeign.hs @@ -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 diff --git a/compiler/deSugar/DsListComp.hs b/compiler/deSugar/DsListComp.hs index def390c6c7..f376ef0b4b 100644 --- a/compiler/deSugar/DsListComp.hs +++ b/compiler/deSugar/DsListComp.hs @@ -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 diff --git a/compiler/deSugar/DsUtils.hs b/compiler/deSugar/DsUtils.hs index b78eef4c37..f39d0f2594 100644 --- a/compiler/deSugar/DsUtils.hs +++ b/compiler/deSugar/DsUtils.hs @@ -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), diff --git a/compiler/ghci/ByteCodeGen.hs b/compiler/ghci/ByteCodeGen.hs index 113690780b..86bb72b550 100644 --- a/compiler/ghci/ByteCodeGen.hs +++ b/compiler/ghci/ByteCodeGen.hs @@ -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) diff --git a/compiler/ghci/RtClosureInspect.hs b/compiler/ghci/RtClosureInspect.hs index 4a119a991b..82e0f88d26 100644 --- a/compiler/ghci/RtClosureInspect.hs +++ b/compiler/ghci/RtClosureInspect.hs @@ -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 diff --git a/compiler/hieFile/HieAst.hs b/compiler/hieFile/HieAst.hs index 7fd217cda5..9ac65ce399 100644 --- a/compiler/hieFile/HieAst.hs +++ b/compiler/hieFile/HieAst.hs @@ -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. -- diff --git a/compiler/hieFile/HieUtils.hs b/compiler/hieFile/HieUtils.hs index 5259ea1280..9231317bd0 100644 --- a/compiler/hieFile/HieUtils.hs +++ b/compiler/hieFile/HieUtils.hs @@ -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 diff --git a/compiler/hsSyn/HsUtils.hs b/compiler/hsSyn/HsUtils.hs index 72c70a83ab..7d7ad4411c 100644 --- a/compiler/hsSyn/HsUtils.hs +++ b/compiler/hsSyn/HsUtils.hs @@ -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 diff --git a/compiler/iface/BuildTyCl.hs b/compiler/iface/BuildTyCl.hs index 693e2899c8..4cbcb963d6 100644 --- a/compiler/iface/BuildTyCl.hs +++ b/compiler/iface/BuildTyCl.hs @@ -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 diff --git a/compiler/iface/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs index 3dd8a21173..05f64dff5a 100644 --- a/compiler/iface/IfaceSyn.hs +++ b/compiler/iface/IfaceSyn.hs @@ -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 diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs index f4032d2ae1..985a612940 100644 --- a/compiler/iface/IfaceType.hs +++ b/compiler/iface/IfaceType.hs @@ -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 diff --git a/compiler/iface/TcIface.hs b/compiler/iface/TcIface.hs index 29893ca319..3874d8d6a2 100644 --- a/compiler/iface/TcIface.hs +++ b/compiler/iface/TcIface.hs @@ -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) diff --git a/compiler/iface/ToIface.hs b/compiler/iface/ToIface.hs index 7c8a939965..3779e394cc 100644 --- a/compiler/iface/ToIface.hs +++ b/compiler/iface/ToIface.hs @@ -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) diff --git a/compiler/prelude/PrimOp.hs b/compiler/prelude/PrimOp.hs index 369f17f7f5..fd1bab3386 100644 --- a/compiler/prelude/PrimOp.hs +++ b/compiler/prelude/PrimOp.hs @@ -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: diff --git a/compiler/prelude/TysPrim.hs b/compiler/prelude/TysPrim.hs index ddb1211e2e..d3fd0b949c 100644 --- a/compiler/prelude/TysPrim.hs +++ b/compiler/prelude/TysPrim.hs @@ -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. diff --git a/compiler/prelude/TysWiredIn.hs b/compiler/prelude/TysWiredIn.hs index 5ea1fd04d2..4e7cd84276 100644 --- a/compiler/prelude/TysWiredIn.hs +++ b/compiler/prelude/TysWiredIn.hs @@ -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 - {- ************************************************************************ * * diff --git a/compiler/prelude/TysWiredIn.hs-boot b/compiler/prelude/TysWiredIn.hs-boot index 1481a758b1..4e8ebba223 100644 --- a/compiler/prelude/TysWiredIn.hs-boot +++ b/compiler/prelude/TysWiredIn.hs-boot @@ -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 diff --git a/compiler/simplCore/SimplUtils.hs b/compiler/simplCore/SimplUtils.hs index 4c59bbaa8b..265b0fb5f9 100644 --- a/compiler/simplCore/SimplUtils.hs +++ b/compiler/simplCore/SimplUtils.hs @@ -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) diff --git a/compiler/simplStg/RepType.hs b/compiler/simplStg/RepType.hs index 4d437d3b7c..d93d716b4b 100644 --- a/compiler/simplStg/RepType.hs +++ b/compiler/simplStg/RepType.hs @@ -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)) diff --git a/compiler/typecheck/ClsInst.hs b/compiler/typecheck/ClsInst.hs index 516b89849f..9f58a0323a 100644 --- a/compiler/typecheck/ClsInst.hs +++ b/compiler/typecheck/ClsInst.hs @@ -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 diff --git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs index 7efcb971a9..3f119ea3c2 100644 --- a/compiler/typecheck/FamInst.hs +++ b/compiler/typecheck/FamInst.hs @@ -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 diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs index d4348ec29c..77e8cdf0b2 100644 --- a/compiler/typecheck/Inst.hs +++ b/compiler/typecheck/Inst.hs @@ -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 diff --git a/compiler/typecheck/TcArrows.hs b/compiler/typecheck/TcArrows.hs index 96adf46db8..763684bb75 100644 --- a/compiler/typecheck/TcArrows.hs +++ b/compiler/typecheck/TcArrows.hs @@ -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 {- ************************************************************************ diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index 09ef93a6db..9abc04809d 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -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) diff --git a/compiler/typecheck/TcDerivInfer.hs b/compiler/typecheck/TcDerivInfer.hs index ba45e09dc5..d38c922879 100644 --- a/compiler/typecheck/TcDerivInfer.hs +++ b/compiler/typecheck/TcDerivInfer.hs @@ -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 diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index ab48326398..d56e344454 100644 --- a/compiler/typecheck/TcErrors.hs +++ b/compiler/typecheck/TcErrors.hs @@ -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. diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs index 1d6098dbf5..9ee23ebfea 100644 --- a/compiler/typecheck/TcEvidence.hs +++ b/compiler/typecheck/TcEvidence.hs @@ -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 diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs index b87f87771b..d8c53aade2 100644 --- a/compiler/typecheck/TcExpr.hs +++ b/compiler/typecheck/TcExpr.hs @@ -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 }) } diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs index aa2c0202fb..80202b7cbc 100644 --- a/compiler/typecheck/TcFlatten.hs +++ b/compiler/typecheck/TcFlatten.hs @@ -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' #-} diff --git a/compiler/typecheck/TcForeign.hs b/compiler/typecheck/TcForeign.hs index 8038de3d84..4e5feb4d43 100644 --- a/compiler/typecheck/TcForeign.hs +++ b/compiler/typecheck/TcForeign.hs @@ -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 diff --git a/compiler/typecheck/TcGenDeriv.hs b/compiler/typecheck/TcGenDeriv.hs index 701df5ffdc..e4f50ddaf7 100644 --- a/compiler/typecheck/TcGenDeriv.hs +++ b/compiler/typecheck/TcGenDeriv.hs @@ -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 diff --git a/compiler/typecheck/TcGenFunctor.hs b/compiler/typecheck/TcGenFunctor.hs index 41d8eb858a..02f45ad316 100644 --- a/compiler/typecheck/TcGenFunctor.hs +++ b/compiler/typecheck/TcGenFunctor.hs @@ -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 diff --git a/compiler/typecheck/TcHoleErrors.hs b/compiler/typecheck/TcHoleErrors.hs index 843ec84d75..3f2556c8c4 100644 --- a/compiler/typecheck/TcHoleErrors.hs +++ b/compiler/typecheck/TcHoleErrors.hs @@ -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 diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index c40d8b5543..467c60465a 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -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 diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs index c1fd0da4c6..7314dd7f0e 100644 --- a/compiler/typecheck/TcInstDcls.hs +++ b/compiler/typecheck/TcInstDcls.hs @@ -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 diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs index ded352c1f1..19fbadeacf 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -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 diff --git a/compiler/typecheck/TcMatches.hs b/compiler/typecheck/TcMatches.hs index 6bc988a8f5..4286a5463a 100644 --- a/compiler/typecheck/TcMatches.hs +++ b/compiler/typecheck/TcMatches.hs @@ -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 diff --git a/compiler/typecheck/TcPat.hs b/compiler/typecheck/TcPat.hs index ba3603fb42..f24fb4a3d0 100644 --- a/compiler/typecheck/TcPat.hs +++ b/compiler/typecheck/TcPat.hs @@ -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 diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs index 822697faf6..d46ade1028 100644 --- a/compiler/typecheck/TcPatSyn.hs +++ b/compiler/typecheck/TcPatSyn.hs @@ -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 diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs index c76a48631b..76d1510aa3 100644 --- a/compiler/typecheck/TcRnDriver.hs +++ b/compiler/typecheck/TcRnDriver.hs @@ -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 diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index 7c9d70e066..3a7ab5b10b 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -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 {- diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index c5ffb054f2..d4d3d03b40 100644 --- a/compiler/typecheck/TcSMonad.hs +++ b/compiler/typecheck/TcSMonad.hs @@ -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)) diff --git a/compiler/typecheck/TcSigs.hs b/compiler/typecheck/TcSigs.hs index 65c2c60335..027a4013ab 100644 --- a/compiler/typecheck/TcSigs.hs +++ b/compiler/typecheck/TcSigs.hs @@ -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" diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs index 9e23eca1eb..f50b33efc6 100644 --- a/compiler/typecheck/TcSimplify.hs +++ b/compiler/typecheck/TcSimplify.hs @@ -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 diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs index 846b50945a..121193d6e2 100644 --- a/compiler/typecheck/TcSplice.hs +++ b/compiler/typecheck/TcSplice.hs @@ -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' } diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index 8dfdbb2a5e..28b692f2e8 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -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 diff --git a/compiler/typecheck/TcTyDecls.hs b/compiler/typecheck/TcTyDecls.hs index dc983ca403..e40fd3abf4 100644 --- a/compiler/typecheck/TcTyDecls.hs +++ b/compiler/typecheck/TcTyDecls.hs @@ -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 diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index 7fcf30a538..1f6372cd0a 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -64,7 +64,6 @@ module TcType ( tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcFunResultTyN, tcSplitFunTysN, tcSplitTyConApp, tcSplitTyConApp_maybe, - tcRepSplitTyConApp, tcRepSplitTyConApp_maybe, tcRepSplitTyConApp_maybe', tcTyConAppTyCon, tcTyConAppTyCon_maybe, tcTyConAppArgs, tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcRepSplitAppTy_maybe, tcRepGetNumAppTys, @@ -129,16 +128,16 @@ module TcType ( -------------------------------- -- Rexported from Type - Type, PredType, ThetaType, TyCoBinder, ArgFlag(..), + Type, PredType, ThetaType, TyCoBinder, ArgFlag(..), AnonArgFlag(..), mkForAllTy, mkForAllTys, mkTyCoInvForAllTys, mkSpecForAllTys, mkTyCoInvForAllTy, mkInvForAllTy, mkInvForAllTys, - mkFunTy, mkFunTys, + mkVisFunTy, mkVisFunTys, mkInvisFunTy, mkInvisFunTys, mkTyConApp, mkAppTy, mkAppTys, mkTyConTy, mkTyVarTy, mkTyVarTys, mkTyCoVarTy, mkTyCoVarTys, - isClassPred, isEqPred, isNomEqPred, isIPPred, + isClassPred, isEqPrimPred, isIPPred, isEqPred, isEqPredClass, mkClassPred, isDictLikeTy, tcSplitDFunTy, tcSplitDFunHead, tcSplitMethodTy, @@ -916,7 +915,7 @@ tcTyFamInstsAndVisX = go go _ (LitTy {}) = [] go is_invis_arg (ForAllTy bndr ty) = go is_invis_arg (binderType bndr) ++ go is_invis_arg ty - go is_invis_arg (FunTy ty1 ty2) = go is_invis_arg ty1 + go is_invis_arg (FunTy _ ty1 ty2) = go is_invis_arg ty1 ++ go is_invis_arg ty2 go is_invis_arg ty@(AppTy _ _) = let (ty_head, ty_args) = splitAppTys ty @@ -983,7 +982,7 @@ exactTyCoVarsOfType ty go (TyConApp _ tys) = exactTyCoVarsOfTypes tys go (LitTy {}) = emptyVarSet go (AppTy fun arg) = go fun `unionVarSet` go arg - go (FunTy arg res) = go arg `unionVarSet` go res + go (FunTy _ arg res) = go arg `unionVarSet` go res go (ForAllTy bndr ty) = delBinderVar (go ty) bndr `unionVarSet` go (binderType bndr) go (CastTy ty co) = go ty `unionVarSet` goCo co go (CoercionTy co) = goCo co @@ -1037,14 +1036,14 @@ anyRewritableTyVar ignore_cos role pred ty go_tv rl bvs tv | tv `elemVarSet` bvs = False | otherwise = pred rl tv - go rl bvs (TyVarTy tv) = go_tv rl bvs tv - go _ _ (LitTy {}) = False - go rl bvs (TyConApp tc tys) = go_tc rl bvs tc tys - go rl bvs (AppTy fun arg) = go rl bvs fun || go NomEq bvs arg - go rl bvs (FunTy arg res) = go rl bvs arg || go rl bvs res - go rl bvs (ForAllTy tv ty) = go rl (bvs `extendVarSet` binderVar tv) ty - go rl bvs (CastTy ty co) = go rl bvs ty || go_co rl bvs co - go rl bvs (CoercionTy co) = go_co rl bvs co -- ToDo: check + go rl bvs (TyVarTy tv) = go_tv rl bvs tv + go _ _ (LitTy {}) = False + go rl bvs (TyConApp tc tys) = go_tc rl bvs tc tys + go rl bvs (AppTy fun arg) = go rl bvs fun || go NomEq bvs arg + go rl bvs (FunTy _ arg res) = go rl bvs arg || go rl bvs res + go rl bvs (ForAllTy tv ty) = go rl (bvs `extendVarSet` binderVar tv) ty + go rl bvs (CastTy ty co) = go rl bvs ty || go_co rl bvs co + go rl bvs (CoercionTy co) = go_co rl bvs co -- ToDo: check go_tc NomEq bvs _ tys = any (go NomEq bvs) tys go_tc ReprEq bvs tc tys = any (go_arg bvs) @@ -1274,7 +1273,7 @@ mkSpecSigmaTy :: [TyVar] -> [PredType] -> Type -> Type mkSpecSigmaTy tyvars preds ty = mkSigmaTy (mkTyCoVarBinders Specified tyvars) preds ty mkPhiTy :: [PredType] -> Type -> Type -mkPhiTy = mkFunTys +mkPhiTy = mkInvisFunTys --------------- getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to @@ -1284,7 +1283,7 @@ getDFunTyKey (TyVarTy tv) = getOccName tv getDFunTyKey (TyConApp tc _) = getOccName tc getDFunTyKey (LitTy x) = getDFunTyLitKey x getDFunTyKey (AppTy fun _) = getDFunTyKey fun -getDFunTyKey (FunTy _ _) = getOccName funTyCon +getDFunTyKey (FunTy {}) = getOccName funTyCon getDFunTyKey (ForAllTy _ t) = getDFunTyKey t getDFunTyKey (CastTy ty _) = getDFunTyKey ty getDFunTyKey t@(CoercionTy _) = pprPanic "getDFunTyKey" (ppr t) @@ -1370,8 +1369,9 @@ tcSplitPredFunTy_maybe :: Type -> Maybe (PredType, Type) -- Split off the first predicate argument from a type tcSplitPredFunTy_maybe ty | Just ty' <- tcView ty = tcSplitPredFunTy_maybe ty' -tcSplitPredFunTy_maybe (FunTy arg res) - | isPredTy arg = Just (arg, res) +tcSplitPredFunTy_maybe (FunTy { ft_af = InvisArg + , ft_arg = arg, ft_res = res }) + = Just (arg, res) tcSplitPredFunTy_maybe _ = Nothing @@ -1414,7 +1414,7 @@ tcSplitNestedSigmaTys ty -- underneath it. | Just (arg_tys, tvs1, theta1, rho1) <- tcDeepSplitSigmaTy_maybe ty = let (tvs2, theta2, rho2) = tcSplitNestedSigmaTys rho1 - in (tvs1 ++ tvs2, theta1 ++ theta2, mkFunTys arg_tys rho2) + in (tvs1 ++ tvs2, theta1 ++ theta2, mkVisFunTys arg_tys rho2) -- If there's no forall, we're done. | otherwise = ([], [], ty) @@ -1448,8 +1448,9 @@ tcTyConAppTyCon_maybe ty | Just ty' <- tcView ty = tcTyConAppTyCon_maybe ty' tcTyConAppTyCon_maybe (TyConApp tc _) = Just tc -tcTyConAppTyCon_maybe (FunTy _ _) - = Just funTyCon +tcTyConAppTyCon_maybe (FunTy { ft_af = VisArg }) + = Just funTyCon -- (=>) is /not/ a TyCon in its own right + -- C.f. tcRepSplitAppTy_maybe tcTyConAppTyCon_maybe _ = Nothing @@ -1463,27 +1464,6 @@ tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of Just stuff -> stuff Nothing -> pprPanic "tcSplitTyConApp" (pprType ty) --- | Like 'tcRepSplitTyConApp_maybe', but returns 'Nothing' if, --- --- 1. the type is structurally not a type constructor application, or --- --- 2. the type is a function type (e.g. application of 'funTyCon'), but we --- currently don't even enough information to fully determine its RuntimeRep --- variables. For instance, @FunTy (a :: k) Int@. --- --- By contrast 'tcRepSplitTyConApp_maybe' panics in the second case. --- --- The behavior here is needed during canonicalization; see Note [FunTy and --- decomposing tycon applications] in TcCanonical for details. -tcRepSplitTyConApp_maybe' :: HasCallStack => Type -> Maybe (TyCon, [Type]) -tcRepSplitTyConApp_maybe' (TyConApp tc tys) = Just (tc, tys) -tcRepSplitTyConApp_maybe' (FunTy arg res) - | Just arg_rep <- getRuntimeRep_maybe arg - , Just res_rep <- getRuntimeRep_maybe res - = Just (funTyCon, [arg_rep, res_rep, arg, res]) -tcRepSplitTyConApp_maybe' _ = Nothing - - ----------------------- tcSplitFunTys :: Type -> ([Type], Type) tcSplitFunTys ty = case tcSplitFunTy_maybe ty of @@ -1493,10 +1473,12 @@ tcSplitFunTys ty = case tcSplitFunTy_maybe ty of (args,res') = tcSplitFunTys res tcSplitFunTy_maybe :: Type -> Maybe (Type, Type) -tcSplitFunTy_maybe ty | Just ty' <- tcView ty = tcSplitFunTy_maybe ty' -tcSplitFunTy_maybe (FunTy arg res) | not (isPredTy arg) = Just (arg, res) -tcSplitFunTy_maybe _ = Nothing - -- Note the tcTypeKind guard +tcSplitFunTy_maybe ty + | Just ty' <- tcView ty = tcSplitFunTy_maybe ty' +tcSplitFunTy_maybe (FunTy { ft_af = af, ft_arg = arg, ft_res = res }) + | VisArg <- af = Just (arg, res) +tcSplitFunTy_maybe _ = Nothing + -- Note the VisArg guard -- Consider (?x::Int) => Bool -- We don't want to treat this as a function type! -- A concrete example is test tc230: @@ -1698,10 +1680,10 @@ tc_eq_type keep_syns vis_only orig_ty1 orig_ty2 -- Make sure we handle all FunTy cases since falling through to the -- AppTy case means that tcRepSplitAppTy_maybe may see an unzonked -- kind variable, which causes things to blow up. - go env (FunTy arg1 res1) (FunTy arg2 res2) + go env (FunTy _ arg1 res1) (FunTy _ arg2 res2) = go env arg1 arg2 && go env res1 res2 - go env ty (FunTy arg res) = eqFunTy env arg res ty - go env (FunTy arg res) ty = eqFunTy env arg res ty + go env ty (FunTy _ arg res) = eqFunTy env arg res ty + go env (FunTy _ arg res) ty = eqFunTy env arg res ty -- See Note [Equality on AppTys] in Type go env (AppTy s1 t1) ty2 @@ -2001,7 +1983,7 @@ isInsolubleOccursCheck eq_rel tv ty go (AppTy t1 t2) = case eq_rel of -- See Note [AppTy and ReprEq] NomEq -> go t1 || go t2 ReprEq -> go t1 - go (FunTy t1 t2) = go t1 || go t2 + go (FunTy _ t1 t2) = go t1 || go t2 go (ForAllTy (Bndr tv' _) inner_ty) | tv' == tv = False | otherwise = go (varType tv') || go inner_ty @@ -2121,15 +2103,15 @@ isSigmaTy :: TcType -> Bool -- *necessarily* have any foralls. E.g -- f :: (?x::Int) => Int -> Int isSigmaTy ty | Just ty' <- tcView ty = isSigmaTy ty' -isSigmaTy (ForAllTy {}) = True -isSigmaTy (FunTy a _) = isPredTy a -isSigmaTy _ = False +isSigmaTy (ForAllTy {}) = True +isSigmaTy (FunTy { ft_af = InvisArg }) = True +isSigmaTy _ = False isRhoTy :: TcType -> Bool -- True of TcRhoTypes; see Note [TcRhoType] isRhoTy ty | Just ty' <- tcView ty = isRhoTy ty' -isRhoTy (ForAllTy {}) = False -isRhoTy (FunTy a r) = not (isPredTy a) && isRhoTy r -isRhoTy _ = True +isRhoTy (ForAllTy {}) = False +isRhoTy (FunTy { ft_af = VisArg, ft_res = r }) = isRhoTy r +isRhoTy _ = True -- | Like 'isRhoTy', but also says 'True' for 'Infer' types isRhoExpTy :: ExpType -> Bool @@ -2140,9 +2122,9 @@ isOverloadedTy :: Type -> Bool -- Yes for a type of a function that might require evidence-passing -- Used only by bindLocalMethods isOverloadedTy ty | Just ty' <- tcView ty = isOverloadedTy ty' -isOverloadedTy (ForAllTy _ ty) = isOverloadedTy ty -isOverloadedTy (FunTy a _) = isPredTy a -isOverloadedTy _ = False +isOverloadedTy (ForAllTy _ ty) = isOverloadedTy ty +isOverloadedTy (FunTy { ft_af = InvisArg }) = True +isOverloadedTy _ = False isFloatTy, isDoubleTy, isIntegerTy, isIntTy, isWordTy, isBoolTy, isUnitTy, isCharTy, isAnyTy :: Type -> Bool @@ -2570,7 +2552,7 @@ sizeType = go -- size ordering is sound, but why is this better? -- I came across this when investigating #14010. go (LitTy {}) = 1 - go (FunTy arg res) = go arg + go res + 1 + go (FunTy _ arg res) = go arg + go res + 1 go (AppTy fun arg) = go fun + go arg go (ForAllTy (Bndr tv vis) ty) | isVisibleArgFlag vis = go (tyVarKind tv) + go ty + 1 diff --git a/compiler/typecheck/TcTypeable.hs b/compiler/typecheck/TcTypeable.hs index d6b1f70e38..cf7700a98f 100644 --- a/compiler/typecheck/TcTypeable.hs +++ b/compiler/typecheck/TcTypeable.hs @@ -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 diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs index 6af873e036..8a3e03c09e 100644 --- a/compiler/typecheck/TcUnify.hs +++ b/compiler/typecheck/TcUnify.hs @@ -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 diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs index 218f539c68..8ab63f49cc 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -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 diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs index 733c11977e..254f76ca31 100644 --- a/compiler/types/Coercion.hs +++ b/compiler/types/Coercion.hs @@ -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) diff --git a/compiler/types/FamInstEnv.hs b/compiler/types/FamInstEnv.hs index 1c9727aaec..88f64bfc87 100644 --- a/compiler/types/FamInstEnv.hs +++ b/compiler/types/FamInstEnv.hs @@ -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 diff --git a/compiler/types/Kind.hs b/compiler/types/Kind.hs index 17c8041821..7989265ce0 100644 --- a/compiler/types/Kind.hs +++ b/compiler/types/Kind.hs @@ -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 diff --git a/compiler/types/OptCoercion.hs b/compiler/types/OptCoercion.hs index 0e9a599573..c521a85635 100644 --- a/compiler/types/OptCoercion.hs +++ b/compiler/types/OptCoercion.hs @@ -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" diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs index 9c50d2ee9f..3594c7a3a3 100644 --- a/compiler/types/TyCoRep.hs +++ b/compiler/types/TyCoRep.hs @@ -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 diff --git a/compiler/types/TyCoRep.hs-boot b/compiler/types/TyCoRep.hs-boot index 5af8c1d57f..cdc4cd6d4c 100644 --- a/compiler/types/TyCoRep.hs-boot +++ b/compiler/types/TyCoRep.hs-boot @@ -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 diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs index ca49560eae..4557ad6388 100644 --- a/compiler/types/TyCon.hs +++ b/compiler/types/TyCon.hs @@ -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 diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index 945d7e1a8d..473e9e5ef8 100644 --- a/compiler/types/Type.hs +++ b/compiler/types/Type.hs @@ -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) diff --git a/compiler/types/Unify.hs b/compiler/types/Unify.hs index d13266660b..9720afc582 100644 --- a/compiler/types/Unify.hs +++ b/compiler/types/Unify.hs @@ -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 diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst index c3090b0722..3880cb93cc 100644 --- a/docs/users_guide/glasgow_exts.rst +++ b/docs/users_guide/glasgow_exts.rst @@ -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`` ----------------- diff --git a/testsuite/tests/callarity/unittest/CallArity1.hs b/testsuite/tests/callarity/unittest/CallArity1.hs index 1100ff6a8f..00583d0209 100644 --- a/testsuite/tests/callarity/unittest/CallArity1.hs +++ b/testsuite/tests/callarity/unittest/CallArity1.hs @@ -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)] diff --git a/testsuite/tests/dependent/should_fail/T15215.hs b/testsuite/tests/dependent/should_fail/T15215.hs index 96fe04385b..e4968a1654 100644 --- a/testsuite/tests/dependent/should_fail/T15215.hs +++ b/testsuite/tests/dependent/should_fail/T15215.hs @@ -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 diff --git a/testsuite/tests/dependent/should_fail/T15215.stderr b/testsuite/tests/dependent/should_fail/T15215.stderr index 53aff765a3..be2d7c75e7 100644 --- a/testsuite/tests/dependent/should_fail/T15215.stderr +++ b/testsuite/tests/dependent/should_fail/T15215.stderr @@ -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’ diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T index 9c34ed4263..8a885b39a5 100644 --- a/testsuite/tests/polykinds/all.T +++ b/testsuite/tests/polykinds/all.T @@ -206,4 +206,3 @@ test('T14887a', normal, compile, ['']) test('T14847', normal, compile, ['']) test('T15795', normal, compile, ['']) test('T15795a', normal, compile, ['']) - diff --git a/testsuite/tests/typecheck/should_fail/T12102.hs b/testsuite/tests/typecheck/should_fail/T12102.hs index 6d21fef914..b17c9937c8 100644 --- a/testsuite/tests/typecheck/should_fail/T12102.hs +++ b/testsuite/tests/typecheck/should_fail/T12102.hs @@ -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 index ea3016b21c..0000000000 --- a/testsuite/tests/typecheck/should_fail/T12102.stderr +++ /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’ diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T index bb7ed96327..1a775d3a7c 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -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, ['']) diff --git a/utils/genprimopcode/Main.hs b/utils/genprimopcode/Main.hs index 863a7d239c..d7ae9ffe01 100644 --- a/utils/genprimopcode/Main.hs +++ b/utils/genprimopcode/Main.hs @@ -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") diff --git a/utils/haddock b/utils/haddock -Subproject 1a4715b2c14d6387da91e74560845fb6cbe6808 +Subproject c323c257be0bc118a0501416f06bda8fd51c92f |