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 /compiler/typecheck | |
| 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
Diffstat (limited to 'compiler/typecheck')
32 files changed, 274 insertions, 383 deletions
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 |