diff options
| author | Richard Eisenberg <eir@cis.upenn.edu> | 2014-12-12 17:19:21 -0500 |
|---|---|---|
| committer | Richard Eisenberg <eir@cis.upenn.edu> | 2014-12-12 17:24:37 -0500 |
| commit | 0cc47eb90805f3e166ac4d3991e66d3346ca05e7 (patch) | |
| tree | 1ed6c6dd440e1dcdd32f16d547b3e0c4ceeddbda | |
| parent | 058262bac0bbcd65f40703bf8047238ffa30d2c3 (diff) | |
| download | haskell-0cc47eb90805f3e166ac4d3991e66d3346ca05e7.tar.gz | |
Rewrite `Coercible` solver
Summary:
This is a rewrite of the algorithm to solve for Coercible "instances".
A preliminary form of these ideas is at
https://ghc.haskell.org/trac/ghc/wiki/Design/NewCoercibleSolver
The basic idea here is that the `EqPred` constructor of `PredTree`
now is parameterised by a new type `EqRel` (where
`data EqRel = NomEq | ReprEq`). Thus, every equality constraint can
now talk about nominal equality (the usual case) or representational
equality (the `Coercible` case).
This is a change from the previous
behavior where `Coercible` was just considered a regular class with
a special case in `matchClassInst`.
Because of this change, representational equalities are now
canonicalized just like nominal ones, allowing more equalities
to be solved -- in particular, the case at the top of #9117.
A knock-on effect is that the flattener must be aware of the
choice of equality relation, because the inert set now stores
both representational inert equalities alongside the nominal
inert equalities. Of course, we can use representational equalities
to rewrite only within another representational equality --
thus the parameterization of the flattener.
A nice side effect of this change is that I've introduced a new
type `CtFlavour`, which tracks G vs. W vs. D, removing some ugliness
in the flattener.
This commit includes some refactoring as discussed on D546.
It also removes the ability of Deriveds to rewrite Deriveds.
This fixes bugs #9117 and #8984.
Reviewers: simonpj, austin, nomeata
Subscribers: carter, thomie
Differential Revision: https://phabricator.haskell.org/D546
GHC Trac Issues: #9117, #8984
48 files changed, 1861 insertions, 1153 deletions
diff --git a/compiler/basicTypes/DataCon.hs b/compiler/basicTypes/DataCon.hs index 09196fba52..4323d6d147 100644 --- a/compiler/basicTypes/DataCon.hs +++ b/compiler/basicTypes/DataCon.hs @@ -971,9 +971,9 @@ dataConCannotMatch tys con -- TODO: could gather equalities from superclasses too predEqs pred = case classifyPredType pred of - EqPred ty1 ty2 -> [(ty1, ty2)] - TuplePred ts -> concatMap predEqs ts - _ -> [] + EqPred NomEq ty1 ty2 -> [(ty1, ty2)] + TuplePred ts -> concatMap predEqs ts + _ -> [] {- ************************************************************************ diff --git a/compiler/deSugar/DsBinds.hs b/compiler/deSugar/DsBinds.hs index b2ca4dca2c..f328ce9014 100644 --- a/compiler/deSugar/DsBinds.hs +++ b/compiler/deSugar/DsBinds.hs @@ -951,9 +951,7 @@ ds_tc_coercion subst tc_co where go (TcRefl r ty) = Refl r (Coercion.substTy subst ty) go (TcTyConAppCo r tc cos) = mkTyConAppCo r tc (map go cos) - go (TcAppCo co1 co2) = let leftCo = go co1 - rightRole = nextRole leftCo in - mkAppCoFlexible leftCo rightRole (go co2) + go (TcAppCo co1 co2) = mkAppCo (go co1) (go co2) go (TcForAllCo tv co) = mkForAllCo tv' (ds_tc_coercion subst' co) where (subst', tv') = Coercion.substTyVarBndr subst tv @@ -969,6 +967,7 @@ ds_tc_coercion subst tc_co go (TcCastCo co1 co2) = mkCoCast (go co1) (go co2) go (TcCoVarCo v) = ds_ev_id subst v go (TcAxiomRuleCo co ts cs) = AxiomRuleCo co (map (Coercion.substTy subst) ts) (map go cs) + go (TcCoercion co) = co ds_co_binds :: TcEvBinds -> CvSubst ds_co_binds (EvBinds bs) = foldl ds_scc subst (sccEvBinds bs) diff --git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs index 3a16ff0218..b3e7525856 100644 --- a/compiler/typecheck/FamInst.hs +++ b/compiler/typecheck/FamInst.hs @@ -6,18 +6,17 @@ module FamInst ( FamInstEnvs, tcGetFamInstEnvs, checkFamInstConsistency, tcExtendLocalFamInstEnv, tcLookupFamInst, - tcLookupDataFamInst, tcInstNewTyConTF_maybe, tcInstNewTyCon_maybe, + tcLookupDataFamInst, tcLookupDataFamInst_maybe, + tcInstNewTyCon_maybe, tcTopNormaliseNewTypeTF_maybe, newFamInst ) where import HscTypes import FamInstEnv import InstEnv( roughMatchTcs ) -import Coercion( pprCoAxBranchHdr ) +import Coercion hiding ( substTy ) import TcEvidence import LoadIface -import Type( applyTysX ) -import TypeRep import TcRnMonad import TyCon import CoAxiom @@ -27,6 +26,8 @@ import Outputable import UniqFM import FastString import Util +import RdrName +import DataCon ( dataConName ) import Maybes import TcMType import TcType @@ -34,6 +35,7 @@ import Name import Control.Monad import Data.Map (Map) import qualified Data.Map as Map +import Control.Arrow ( first, second ) #include "HsVersions.h" @@ -216,45 +218,80 @@ tcLookupFamInst fam_envs tycon tys -- Checks for a newtype, and for being saturated -- Just like Coercion.instNewTyCon_maybe, but returns a TcCoercion tcInstNewTyCon_maybe :: TyCon -> [TcType] -> Maybe (TcType, TcCoercion) -tcInstNewTyCon_maybe tc tys - | Just (tvs, ty, co_tc) <- unwrapNewTyConEtad_maybe tc -- Check for newtype - , tvs `leLength` tys -- Check saturated enough - = Just (applyTysX tvs ty tys, mkTcUnbranchedAxInstCo Representational co_tc tys) - | otherwise - = Nothing +tcInstNewTyCon_maybe tc tys = fmap (second TcCoercion) $ + instNewTyCon_maybe tc tys +-- | Like 'tcLookupDataFamInst_maybe', but returns the arguments back if +-- there is no data family to unwrap. tcLookupDataFamInst :: FamInstEnvs -> TyCon -> [TcType] -> (TyCon, [TcType], TcCoercion) +tcLookupDataFamInst fam_inst_envs tc tc_args + | Just (rep_tc, rep_args, co) + <- tcLookupDataFamInst_maybe fam_inst_envs tc tc_args + = (rep_tc, rep_args, TcCoercion co) + | otherwise + = (tc, tc_args, mkTcRepReflCo (mkTyConApp tc tc_args)) + +tcLookupDataFamInst_maybe :: FamInstEnvs -> TyCon -> [TcType] + -> Maybe (TyCon, [TcType], Coercion) -- ^ Converts a data family type (eg F [a]) to its representation type (eg FList a) -- and returns a coercion between the two: co :: F [a] ~R FList a --- If there is no instance, or it's not a data family, just return --- Refl coercion and the original inputs -tcLookupDataFamInst fam_inst_envs tc tc_args +tcLookupDataFamInst_maybe fam_inst_envs tc tc_args | isDataFamilyTyCon tc , match : _ <- lookupFamInstEnv fam_inst_envs tc tc_args , FamInstMatch { fim_instance = rep_fam , fim_tys = rep_args } <- match , let co_tc = famInstAxiom rep_fam rep_tc = dataFamInstRepTyCon rep_fam - co = mkTcUnbranchedAxInstCo Representational co_tc rep_args - = (rep_tc, rep_args, co) + co = mkUnbranchedAxInstCo Representational co_tc rep_args + = Just (rep_tc, rep_args, co) | otherwise - = (tc, tc_args, mkTcNomReflCo (mkTyConApp tc tc_args)) - -tcInstNewTyConTF_maybe :: FamInstEnvs -> TcType -> Maybe (TyCon, TcType, TcCoercion) --- ^ If (instNewTyConTF_maybe envs ty) returns Just (ty', co) --- then co :: ty ~R ty' --- ty is (D tys) is a newtype (possibly after looking through the type family D) --- ty' is the RHS type of the of (D tys) newtype -tcInstNewTyConTF_maybe fam_envs ty - | Just (tc, tc_args) <- tcSplitTyConApp_maybe ty - , let (rep_tc, rep_tc_args, fam_co) = tcLookupDataFamInst fam_envs tc tc_args - , Just (inner_ty, nt_co) <- tcInstNewTyCon_maybe rep_tc rep_tc_args - = Just (rep_tc, inner_ty, fam_co `mkTcTransCo` nt_co) - | otherwise = Nothing +-- | Get rid of top-level newtypes, potentially looking through newtype +-- instances. Only unwraps newtypes that are in scope. This is used +-- for solving for `Coercible` in the solver. This version is careful +-- not to unwrap data/newtype instances if it can't continue unwrapping. +-- Such care is necessary for proper error messages. +-- +-- Does not look through type families. Does not normalise arguments to a +-- tycon. +-- +-- Always produces a representational coercion. +tcTopNormaliseNewTypeTF_maybe :: FamInstEnvs + -> GlobalRdrEnv + -> Type + -> Maybe (TcCoercion, Type) +tcTopNormaliseNewTypeTF_maybe faminsts rdr_env ty +-- cf. FamInstEnv.topNormaliseType_maybe and Coercion.topNormaliseNewType_maybe + = fmap (first TcCoercion) $ topNormaliseTypeX_maybe stepper ty + where + stepper + = unwrap_newtype + `composeSteppers` + \ rec_nts tc tys -> + case tcLookupDataFamInst_maybe faminsts tc tys of + Just (tc', tys', co) -> + modifyStepResultCo (co `mkTransCo`) + (unwrap_newtype rec_nts tc' tys') + Nothing -> NS_Done + + unwrap_newtype rec_nts tc tys + | data_cons_in_scope tc + = unwrapNewTypeStepper rec_nts tc tys + + | otherwise + = NS_Done + + data_cons_in_scope :: TyCon -> Bool + data_cons_in_scope tc + = isWiredInName (tyConName tc) || + (not (isAbstractTyCon tc) && all in_scope data_con_names) + where + data_con_names = map dataConName (tyConDataCons tc) + in_scope dc = not $ null $ lookupGRE_Name rdr_env dc + {- ************************************************************************ * * diff --git a/compiler/typecheck/FunDeps.hs b/compiler/typecheck/FunDeps.hs index 65767faded..a55fa2e3b8 100644 --- a/compiler/typecheck/FunDeps.hs +++ b/compiler/typecheck/FunDeps.hs @@ -480,9 +480,9 @@ oclose preds fixed_tvs do let (cls_tvs, cls_fds) = classTvsFds cls fd <- cls_fds return (instFD fd cls_tvs tys) - EqPred t1 t2 -> [([t1],[t2]), ([t2],[t1])] - TuplePred ts -> concatMap determined ts - _ -> [] + EqPred NomEq t1 t2 -> [([t1],[t2]), ([t2],[t1])] + TuplePred ts -> concatMap determined ts + _ -> [] {- ************************************************************************ diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs index afe466bb76..2c1c9cc90b 100644 --- a/compiler/typecheck/Inst.hs +++ b/compiler/typecheck/Inst.hs @@ -220,8 +220,21 @@ instCallConstraints orig preds = do { co <- unifyType ty1 ty2 ; return (EvCoercion co) } | otherwise - = do { ev_var <- emitWanted orig pred + = do { ev_var <- emitWanted modified_orig pred ; return (EvId ev_var) } + where + -- Coercible constraints appear as normal class constraints, but + -- are aggressively canonicalized and manipulated during solving. + -- The final equality to solve may barely resemble the initial + -- constraint. Here, we remember the initial constraint in a + -- CtOrigin for better error messages. It's perhaps worthwhile + -- considering making this approach general, for other class + -- constraints, too. + modified_orig + | Just (Representational, ty1, ty2) <- getEqPredTys_maybe pred + = CoercibleOrigin ty1 ty2 + | otherwise + = orig ---------------- instStupidTheta :: CtOrigin -> TcThetaType -> TcM () diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index 749748ff80..0cc62e40c3 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -19,17 +19,25 @@ import TcEvidence import Class import TyCon import TypeRep +import Coercion +import FamInstEnv ( FamInstEnvs ) +import FamInst ( tcTopNormaliseNewTypeTF_maybe ) import Var -import Name( isSystemName ) +import DataCon ( dataConName ) +import Name( isSystemName, nameOccName ) import OccName( OccName ) import Outputable import Control.Monad import DynFlags( DynFlags ) import VarSet +import RdrName import Pair import Util +import MonadUtils ( zipWith3M, zipWith3M_ ) +import Data.List ( zip4 ) import BasicTypes +import Data.Maybe ( isJust ) import FastString {- @@ -140,9 +148,10 @@ canonicalize (CDictCan { cc_ev = ev canClass ev cls xis -- Do not add any superclasses canonicalize (CTyEqCan { cc_ev = ev , cc_tyvar = tv - , cc_rhs = xi }) + , cc_rhs = xi + , cc_eq_rel = eq_rel }) = {-# SCC "canEqLeafTyVarEq" #-} - canEqTyVar ev NotSwapped tv xi xi + canEqTyVar ev eq_rel NotSwapped tv xi xi canonicalize (CFunEqCan { cc_ev = ev , cc_fun = fn @@ -160,11 +169,14 @@ canEvNC :: CtEvidence -> TcS (StopOrContinue Ct) -- Called only for non-canonical EvVars canEvNC ev = case classifyPredType (ctEvPred ev) of - ClassPred cls tys -> traceTcS "canEvNC:cls" (ppr cls <+> ppr tys) >> canClassNC ev cls tys - EqPred ty1 ty2 -> traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2) >> canEqNC ev ty1 ty2 - TuplePred tys -> traceTcS "canEvNC:tup" (ppr tys) >> canTuple ev tys - IrredPred {} -> traceTcS "canEvNC:irred" (ppr (ctEvPred ev)) >> canIrred ev - + ClassPred cls tys -> do traceTcS "canEvNC:cls" (ppr cls <+> ppr tys) + canClassNC ev cls tys + EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2) + canEqNC ev eq_rel ty1 ty2 + TuplePred tys -> do traceTcS "canEvNC:tup" (ppr tys) + canTuple ev tys + IrredPred {} -> do traceTcS "canEvNC:irred" (ppr (ctEvPred ev)) + canIrred ev {- ************************************************************************ * * @@ -204,7 +216,9 @@ canClassNC ev cls tys `andWhenContinue` emitSuperclasses canClass ev cls tys - = do { (xis, cos) <- flattenMany FM_FlattenAll ev tys + = -- all classes do *nominal* matching + ASSERT2( ctEvRole ev == Nominal, ppr ev $$ ppr cls $$ ppr tys ) + do { (xis, cos) <- flattenMany FM_FlattenAll ev (repeat Nominal) tys ; let co = mkTcTyConAppCo Nominal (classTyCon cls) cos xi = mkClassPred cls xis mk_ct new_ev = CDictCan { cc_ev = new_ev @@ -320,7 +334,8 @@ is_improvement_pty :: PredType -> Bool -- Either it's an equality, or has some functional dependency is_improvement_pty ty = go (classifyPredType ty) where - go (EqPred t1 t2) = not (t1 `tcEqType` t2) + go (EqPred NomEq t1 t2) = not (t1 `tcEqType` t2) + go (EqPred ReprEq _ _) = False go (ClassPred cls _tys) = not $ null fundeps where (_,fundeps) = classTvsFds cls go (TuplePred ts) = any is_improvement_pty ts @@ -340,31 +355,24 @@ canIrred old_ev = do { let old_ty = ctEvPred old_ev ; traceTcS "can_pred" (text "IrredPred = " <+> ppr old_ty) ; (xi,co) <- flatten FM_FlattenAll old_ev old_ty -- co :: xi ~ old_ty - -- Flatten (F [a]), say, so that it can reduce to Eq a - ; mb <- rewriteEvidence old_ev xi co - ; case mb of { - Stop ev s -> return (Stop ev s) ; - ContinueWith new_ev -> - + ; rewriteEvidence old_ev xi co `andWhenContinue` \ new_ev -> do { -- Re-classify, in case flattening has improved its shape ; case classifyPredType (ctEvPred new_ev) of - ClassPred cls tys -> canClassNC new_ev cls tys - TuplePred tys -> canTuple new_ev tys - EqPred ty1 ty2 -> canEqNC new_ev ty1 ty2 - _ -> continueWith $ - CIrredEvCan { cc_ev = new_ev } } } } + ClassPred cls tys -> canClassNC new_ev cls tys + TuplePred tys -> canTuple new_ev tys + EqPred eq_rel ty1 ty2 -> canEqNC new_ev eq_rel ty1 ty2 + _ -> continueWith $ + CIrredEvCan { cc_ev = new_ev } } } canHole :: CtEvidence -> OccName -> HoleSort -> TcS (StopOrContinue Ct) canHole ev occ hole_sort = do { let ty = ctEvPred ev ; (xi,co) <- flatten FM_SubstOnly ev ty -- co :: xi ~ ty - ; mb <- rewriteEvidence ev xi co - ; case mb of - ContinueWith new_ev -> do { emitInsoluble (CHoleCan { cc_ev = new_ev - , cc_occ = occ - , cc_hole = hole_sort }) - ; stopWith new_ev "Emit insoluble hole" } - Stop ev s -> return (Stop ev s) } -- Found a cached copy; won't happen + ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev -> + do { emitInsoluble (CHoleCan { cc_ev = new_ev + , cc_occ = occ + , cc_hole = hole_sort }) + ; stopWith new_ev "Emit insoluble hole" } } {- ************************************************************************ @@ -374,83 +382,107 @@ canHole ev occ hole_sort ************************************************************************ -} -canEqNC :: CtEvidence -> Type -> Type -> TcS (StopOrContinue Ct) -canEqNC ev ty1 ty2 = can_eq_nc ev ty1 ty1 ty2 ty2 +canEqNC :: CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct) +canEqNC ev eq_rel ty1 ty2 + = can_eq_nc ev eq_rel ty1 ty1 ty2 ty2 -can_eq_nc, can_eq_nc' +can_eq_nc :: CtEvidence + -> EqRel -> Type -> Type -- LHS, after and before type-synonym expansion, resp -> Type -> Type -- RHS, after and before type-synonym expansion, resp -> TcS (StopOrContinue Ct) - -can_eq_nc ev ty1 ps_ty1 ty2 ps_ty2 +can_eq_nc ev eq_rel ty1 ps_ty1 ty2 ps_ty2 = do { traceTcS "can_eq_nc" $ - vcat [ ppr ev, ppr ty1, ppr ps_ty1, ppr ty2, ppr ps_ty2 ] - ; can_eq_nc' ev ty1 ps_ty1 ty2 ps_ty2 } + vcat [ ppr ev, ppr eq_rel, ppr ty1, ppr ps_ty1, ppr ty2, ppr ps_ty2 ] + ; rdr_env <- getGlobalRdrEnvTcS + ; fam_insts <- getFamInstEnvs + ; can_eq_nc' rdr_env fam_insts ev eq_rel ty1 ps_ty1 ty2 ps_ty2 } + +can_eq_nc' + :: GlobalRdrEnv -- needed to see which newtypes are in scope + -> FamInstEnvs -- needed to unwrap data instances + -> CtEvidence + -> EqRel + -> Type -> Type -- LHS, after and before type-synonym expansion, resp + -> Type -> Type -- RHS, after and before type-synonym expansion, resp + -> TcS (StopOrContinue Ct) -- Expand synonyms first; see Note [Type synonyms and canonicalization] -can_eq_nc' ev ty1 ps_ty1 ty2 ps_ty2 - | Just ty1' <- tcView ty1 = can_eq_nc ev ty1' ps_ty1 ty2 ps_ty2 - | Just ty2' <- tcView ty2 = can_eq_nc ev ty1 ps_ty1 ty2' ps_ty2 +can_eq_nc' _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2 + | Just ty1' <- tcView ty1 = can_eq_nc ev eq_rel ty1' ps_ty1 ty2 ps_ty2 + | Just ty2' <- tcView ty2 = can_eq_nc ev eq_rel ty1 ps_ty1 ty2' ps_ty2 -- Type family on LHS or RHS take priority over tyvars, -- so that tv ~ F ty gets flattened -- Otherwise F a ~ F a might not get solved! -can_eq_nc' ev (TyConApp fn1 tys1) _ ty2 ps_ty2 - | isTypeFamilyTyCon fn1 = can_eq_fam_nc ev NotSwapped fn1 tys1 ty2 ps_ty2 -can_eq_nc' ev ty1 ps_ty1 (TyConApp fn2 tys2) _ - | isTypeFamilyTyCon fn2 = can_eq_fam_nc ev IsSwapped fn2 tys2 ty1 ps_ty1 +can_eq_nc' _rdr_env _envs ev eq_rel (TyConApp fn1 tys1) _ ty2 ps_ty2 + | isTypeFamilyTyCon fn1 + = can_eq_fam_nc ev eq_rel NotSwapped fn1 tys1 ty2 ps_ty2 +can_eq_nc' _rdr_env _envs ev eq_rel ty1 ps_ty1 (TyConApp fn2 tys2) _ + | isTypeFamilyTyCon fn2 + = can_eq_fam_nc ev eq_rel IsSwapped fn2 tys2 ty1 ps_ty1 + +-- When working with ReprEq, unwrap newtypes next. +-- Otherwise, a ~ Id a wouldn't get solved +can_eq_nc' rdr_env envs ev ReprEq ty1 _ ty2 ps_ty2 + | Just (co, ty1') <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1 + = can_eq_newtype_nc rdr_env ev NotSwapped co ty1 ty1' ty2 ps_ty2 +can_eq_nc' rdr_env envs ev ReprEq ty1 ps_ty1 ty2 _ + | Just (co, ty2') <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2 + = can_eq_newtype_nc rdr_env ev IsSwapped co ty2 ty2' ty1 ps_ty1 -- Type variable on LHS or RHS are next -can_eq_nc' ev (TyVarTy tv1) _ ty2 ps_ty2 - = canEqTyVar ev NotSwapped tv1 ty2 ps_ty2 -can_eq_nc' ev ty1 ps_ty1 (TyVarTy tv2) _ - = canEqTyVar ev IsSwapped tv2 ty1 ps_ty1 +can_eq_nc' _rdr_env _envs ev eq_rel (TyVarTy tv1) _ ty2 ps_ty2 + = canEqTyVar ev eq_rel NotSwapped tv1 ty2 ps_ty2 +can_eq_nc' _rdr_env _envs ev eq_rel ty1 ps_ty1 (TyVarTy tv2) _ + = canEqTyVar ev eq_rel IsSwapped tv2 ty1 ps_ty1 ---------------------- -- Otherwise try to decompose ---------------------- -- Literals -can_eq_nc' ev ty1@(LitTy l1) _ (LitTy l2) _ +can_eq_nc' _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _ | l1 == l2 = do { when (isWanted ev) $ - setEvBind (ctev_evar ev) (EvCoercion (mkTcNomReflCo ty1)) + setEvBind (ctev_evar ev) (EvCoercion $ + mkTcReflCo (eqRelRole eq_rel) ty1) ; stopWith ev "Equal LitTy" } -- Decomposable type constructor applications -- Synonyms and type functions (which are not decomposable) -- have already been dealt with -can_eq_nc' ev (TyConApp tc1 tys1) _ (TyConApp tc2 tys2) _ +can_eq_nc' _rdr_env _envs ev eq_rel (TyConApp tc1 tys1) _ (TyConApp tc2 tys2) _ | isDecomposableTyCon tc1 , isDecomposableTyCon tc2 - = canDecomposableTyConApp ev tc1 tys1 tc2 tys2 + = canDecomposableTyConApp ev eq_rel tc1 tys1 tc2 tys2 -can_eq_nc' ev (TyConApp tc1 _) ps_ty1 (FunTy {}) ps_ty2 +can_eq_nc' _rdr_env _envs ev eq_rel (TyConApp tc1 _) ps_ty1 (FunTy {}) ps_ty2 | isDecomposableTyCon tc1 -- The guard is important -- e.g. (x -> y) ~ (F x y) where F has arity 1 -- should not fail, but get the app/app case - = canEqFailure ev ps_ty1 ps_ty2 + = canEqHardFailure ev eq_rel ps_ty1 ps_ty2 -can_eq_nc' ev (FunTy s1 t1) _ (FunTy s2 t2) _ - = do { canDecomposableTyConAppOK ev funTyCon [s1,t1] [s2,t2] +can_eq_nc' _rdr_env _envs ev eq_rel (FunTy s1 t1) _ (FunTy s2 t2) _ + = do { canDecomposableTyConAppOK ev eq_rel funTyCon [s1,t1] [s2,t2] ; stopWith ev "Decomposed FunTyCon" } - -can_eq_nc' ev (FunTy {}) ps_ty1 (TyConApp tc2 _) ps_ty2 +can_eq_nc' _rdr_env _envs ev eq_rel (FunTy {}) ps_ty1 (TyConApp tc2 _) ps_ty2 | isDecomposableTyCon tc2 - = canEqFailure ev ps_ty1 ps_ty2 + = canEqHardFailure ev eq_rel ps_ty1 ps_ty2 -can_eq_nc' ev s1@(ForAllTy {}) _ s2@(ForAllTy {}) _ +can_eq_nc' _rdr_env _envs ev eq_rel s1@(ForAllTy {}) _ s2@(ForAllTy {}) _ | CtWanted { ctev_loc = loc, ctev_evar = orig_ev } <- ev = do { let (tvs1,body1) = tcSplitForAllTys s1 (tvs2,body2) = tcSplitForAllTys s2 ; if not (equalLength tvs1 tvs2) then - canEqFailure ev s1 s2 + canEqHardFailure ev eq_rel s1 s2 else do { traceTcS "Creating implication for polytype equality" $ ppr ev - ; ev_term <- deferTcSForAllEq Nominal loc (tvs1,body1) (tvs2,body2) + ; ev_term <- deferTcSForAllEq (eqRelRole eq_rel) + loc (tvs1,body1) (tvs2,body2) ; setEvBind orig_ev ev_term ; stopWith ev "Deferred polytype equality" } } | otherwise @@ -458,79 +490,181 @@ can_eq_nc' ev s1@(ForAllTy {}) _ s2@(ForAllTy {}) _ pprEq s1 s2 -- See Note [Do not decompose given polytype equalities] ; stopWith ev "Discard given polytype equality" } -can_eq_nc' ev (AppTy {}) ps_ty1 _ ps_ty2 - | isGiven ev = try_decompose_app ev ps_ty1 ps_ty2 - | otherwise = can_eq_wanted_app ev ps_ty1 ps_ty2 -can_eq_nc' ev _ ps_ty1 (AppTy {}) ps_ty2 - | isGiven ev = try_decompose_app ev ps_ty1 ps_ty2 - | otherwise = can_eq_wanted_app ev ps_ty1 ps_ty2 +can_eq_nc' _rdr_env _envs ev eq_rel (AppTy {}) ps_ty1 _ ps_ty2 + | isGiven ev = try_decompose_app ev eq_rel ps_ty1 ps_ty2 + | otherwise = can_eq_wanted_app ev eq_rel ps_ty1 ps_ty2 +can_eq_nc' _rdr_env _envs ev eq_rel _ ps_ty1 (AppTy {}) ps_ty2 + | isGiven ev = try_decompose_app ev eq_rel ps_ty1 ps_ty2 + | otherwise = can_eq_wanted_app ev eq_rel ps_ty1 ps_ty2 -- Everything else is a definite type error, eg LitTy ~ TyConApp -can_eq_nc' ev _ ps_ty1 _ ps_ty2 - = canEqFailure ev ps_ty1 ps_ty2 +can_eq_nc' _rdr_env _envs ev eq_rel _ ps_ty1 _ ps_ty2 + = canEqHardFailure ev eq_rel ps_ty1 ps_ty2 ------------ -can_eq_fam_nc :: CtEvidence -> SwapFlag +can_eq_fam_nc :: CtEvidence -> EqRel -> SwapFlag -> TyCon -> [TcType] -> TcType -> TcType -> TcS (StopOrContinue Ct) -- Canonicalise a non-canonical equality of form (F tys ~ ty) -- or the swapped version thereof -- Flatten both sides and go round again -can_eq_fam_nc ev swapped fn tys rhs ps_rhs +can_eq_fam_nc ev eq_rel swapped fn tys rhs ps_rhs = do { (xi_lhs, co_lhs) <- flattenFamApp FM_FlattenAll ev fn tys - ; mb_ct <- rewriteEqEvidence ev swapped xi_lhs rhs co_lhs (mkTcNomReflCo rhs) - ; case mb_ct of - Stop ev s -> return (Stop ev s) - ContinueWith new_ev -> can_eq_nc new_ev xi_lhs xi_lhs rhs ps_rhs } + ; rewriteEqEvidence ev eq_rel swapped xi_lhs rhs co_lhs + (mkTcReflCo (eqRelRole eq_rel) rhs) + `andWhenContinue` \ new_ev -> + can_eq_nc new_ev eq_rel xi_lhs xi_lhs rhs ps_rhs } ------------------------------------ --- Dealing with AppTy --- See Note [Canonicalising type applications] +{- +Note [Eager reflexivity check] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have + + newtype X = MkX (Int -> X) + +and + + [W] X ~R X -can_eq_wanted_app :: CtEvidence -> TcType -> TcType +Naively, we would start unwrapping X and end up in a loop. Instead, +we do this eager reflexivity check. This is necessary only for representational +equality because the flattener technology deals with the similar case +(recursive type families) for nominal equality. + +As an alternative, suppose we also have + + newtype Y = MkY (Int -> Y) + +and now wish to prove + + [W] X ~R Y + +This new Wanted will loop, expanding out the newtypes ever deeper looking +for a solid match or a solid discrepancy. Indeed, there is something +appropriate to this looping, because X and Y *do* have the same representation, +in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized +coercion will ever witness it. This loop won't actually cause GHC to hang, +though, because of the stack-blowing check in can_eq_newtype_nc, along +with the fact that rewriteEqEvidence bumps the stack depth. + +Note [AppTy reflexivity check] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider trying to prove (f a) ~R (f a). The AppTys in there can't +be decomposed, because representational equality isn't congruent with respect +to AppTy. So, when canonicalising the equality above, we get stuck and +would normally produce a CIrredEvCan. However, we really do want to +be able to solve (f a) ~R (f a). So, in the representational case only, +we do a reflexivity check. + +(This would be sound in the nominal case, but unnecessary, and I [Richard +E.] am worried that it would slow down the common case.) +-} + +------------------------ +-- | We're able to unwrap a newtype. Update the bits accordingly. +can_eq_newtype_nc :: GlobalRdrEnv + -> CtEvidence -- ^ :: ty1 ~ ty2 + -> SwapFlag + -> TcCoercion -- ^ :: ty1 ~ ty1' + -> TcType -- ^ ty1 + -> TcType -- ^ ty1' + -> TcType -- ^ ty2 + -> TcType -- ^ ty2, with type synonyms + -> TcS (StopOrContinue Ct) +can_eq_newtype_nc rdr_env ev swapped co ty1 ty1' ty2 ps_ty2 + = do { traceTcS "can_eq_newtype_nc" $ + vcat [ ppr ev, ppr swapped, ppr co, ppr ty1', ppr ty2 ] + + -- check for blowing our stack: + -- See Note [Eager reflexivity check] for an example of + -- when this is necessary + ; dflags <- getDynFlags + ; if isJust $ subGoalDepthExceeded (maxSubGoalDepth dflags) + (ctLocDepth (ctEvLoc ev)) + then do { emitInsoluble (mkNonCanonical ev) + ; stopWith ev "unwrapping newtypes blew stack" } + else do + { if ty1 `eqType` ty2 -- See Note [Eager reflexivity check] + then canEqReflexive ev ReprEq ty1 + else do + { markDataConsAsUsed rdr_env (tyConAppTyCon ty1) + -- we have actually used the newtype constructor here, so + -- make sure we don't warn about importing it! + + ; rewriteEqEvidence ev ReprEq swapped ty1' ps_ty2 + (mkTcSymCo co) (mkTcReflCo Representational ps_ty2) + `andWhenContinue` \ new_ev -> + can_eq_nc new_ev ReprEq ty1' ty1' ty2 ps_ty2 }}} + +-- | Mark all the datacons of the given 'TyCon' as used in this module, +-- avoiding "redundant import" warnings. +markDataConsAsUsed :: GlobalRdrEnv -> TyCon -> TcS () +markDataConsAsUsed rdr_env tc = addUsedRdrNamesTcS + [ mkRdrQual (is_as (is_decl imp_spec)) occ + | dc <- tyConDataCons tc + , let dc_name = dataConName dc + occ = nameOccName dc_name + , gre : _ <- return $ lookupGRE_Name rdr_env dc_name + , Imported (imp_spec:_) <- return $ gre_prov gre ] + +------------------------------------------------- +can_eq_wanted_app :: CtEvidence -> EqRel -> TcType -> TcType -> TcS (StopOrContinue Ct) -- One or the other is an App; neither is a type variable -- See Note [Canonicalising type applications] -can_eq_wanted_app ev ty1 ty2 +can_eq_wanted_app ev eq_rel ty1 ty2 = do { (xi1, co1) <- flatten FM_FlattenAll ev ty1 ; (xi2, co2) <- flatten FM_FlattenAll ev ty2 - ; mb_ct <- rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2 - ; case mb_ct of { - Stop ev s -> return (Stop ev s) ; - ContinueWith new_ev -> try_decompose_app new_ev xi1 xi2 } } + ; rewriteEqEvidence ev eq_rel NotSwapped xi1 xi2 co1 co2 + `andWhenContinue` \ new_ev -> + try_decompose_app new_ev eq_rel xi1 xi2 } -try_decompose_app :: CtEvidence -> TcType -> TcType -> TcS (StopOrContinue Ct) +try_decompose_app :: CtEvidence -> EqRel + -> TcType -> TcType -> TcS (StopOrContinue Ct) -- Preconditions: neither is a type variable -- so can't turn it into an application if it -- doesn't look like one already -- See Note [Canonicalising type applications] -try_decompose_app ev ty1 ty2 +try_decompose_app ev NomEq ty1 ty2 = try_decompose_nom_app ev ty1 ty2 +try_decompose_app ev ReprEq ty1 ty2 + | ty1 `eqType` ty2 -- See Note [AppTy reflexivity check] + = canEqReflexive ev ReprEq ty1 + + | otherwise + = canEqFailure ev ReprEq ty1 ty2 + +try_decompose_nom_app :: CtEvidence + -> TcType -> TcType -> TcS (StopOrContinue Ct) +-- Preconditions: like try_decompose_app, but also +-- ev has a nominal role +-- See Note [Canonicalising type applications] +try_decompose_nom_app ev ty1 ty2 | AppTy s1 t1 <- ty1 = case tcSplitAppTy_maybe ty2 of - Nothing -> canEqFailure ev ty1 ty2 + Nothing -> canEqHardFailure ev NomEq ty1 ty2 Just (s2,t2) -> do_decompose s1 t1 s2 t2 | AppTy s2 t2 <- ty2 = case tcSplitAppTy_maybe ty1 of - Nothing -> canEqFailure ev ty1 ty2 + Nothing -> canEqHardFailure ev NomEq ty1 ty2 Just (s1,t1) -> do_decompose s1 t1 s2 t2 | otherwise -- Neither is an AppTy - = canEqNC ev ty1 ty2 + = canEqNC ev NomEq ty1 ty2 where -- do_decompose is like xCtEvidence, but recurses -- to try_decompose_app to decompose a chain of AppTys do_decompose s1 t1 s2 t2 | CtDerived { ctev_loc = loc } <- ev = do { emitNewDerived loc (mkTcEqPred t1 t2) - ; try_decompose_app ev s1 s2 } + ; try_decompose_nom_app ev s1 s2 } | CtWanted { ctev_evar = evar, ctev_loc = loc } <- ev = do { ev_s <- newWantedEvVarNC loc (mkTcEqPred s1 s2) - ; co_t <- unifyWanted loc t1 t2 + ; co_t <- unifyWanted loc Nominal t1 t2 ; let co = mkTcAppCo (ctEvCoercion ev_s) co_t ; setEvBind evar (EvCoercion co) - ; try_decompose_app ev_s s1 s2 } + ; try_decompose_nom_app ev_s s1 s2 } | CtGiven { ctev_evtm = ev_tm, ctev_loc = loc } <- ev = do { let co = evTermCoercion ev_tm co_s = mkTcLRCo CLeft co @@ -538,59 +672,126 @@ try_decompose_app ev ty1 ty2 ; evar_s <- newGivenEvVar loc (mkTcEqPred s1 s2, EvCoercion co_s) ; evar_t <- newGivenEvVar loc (mkTcEqPred t1 t2, EvCoercion co_t) ; emitWorkNC [evar_t] - ; try_decompose_app evar_s s1 s2 } + ; try_decompose_nom_app evar_s s1 s2 } | otherwise -- Can't happen = error "try_decompose_app" ------------------------ -canDecomposableTyConApp :: CtEvidence +canDecomposableTyConApp :: CtEvidence -> EqRel -> TyCon -> [TcType] -> TyCon -> [TcType] -> TcS (StopOrContinue Ct) -- See Note [Decomposing TyConApps] -canDecomposableTyConApp ev tc1 tys1 tc2 tys2 +canDecomposableTyConApp ev eq_rel tc1 tys1 tc2 tys2 | tc1 /= tc2 || length tys1 /= length tys2 -- Fail straight away for better error messages - = canEqFailure ev (mkTyConApp tc1 tys1) (mkTyConApp tc2 tys2) + = let eq_failure + | isDataFamilyTyCon tc1 || isDataFamilyTyCon tc2 + -- See Note [Use canEqFailure in canDecomposableTyConApp] + = canEqFailure + | otherwise + = canEqHardFailure in + eq_failure ev eq_rel (mkTyConApp tc1 tys1) (mkTyConApp tc2 tys2) + | otherwise - = do { traceTcS "canDecomposableTyConApp" (ppr ev $$ ppr tc1 $$ ppr tys1 $$ ppr tys2) - ; canDecomposableTyConAppOK ev tc1 tys1 tys2 + = do { traceTcS "canDecomposableTyConApp" + (ppr ev $$ ppr eq_rel $$ ppr tc1 $$ ppr tys1 $$ ppr tys2) + ; canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2 ; stopWith ev "Decomposed TyConApp" } -canDecomposableTyConAppOK :: CtEvidence +{- +Note [Use canEqFailure in canDecomposableTyConApp] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We must use canEqFailure, not canEqHardFailure here, because there is +the possibility of success if working with a representational equality. +Here is the case: + + type family TF a where TF Char = Bool + data family DF a + newtype instance DF Bool = MkDF Int + +Suppose we are canonicalising (Int ~R DF (T a)), where we don't yet +know `a`. This is *not* a hard failure, because we might soon learn +that `a` is, in fact, Char, and then the equality succeeds. +-} + +canDecomposableTyConAppOK :: CtEvidence -> EqRel -> TyCon -> [TcType] -> [TcType] -> TcS () -- Precondition: tys1 and tys2 are the same length, hence "OK" -canDecomposableTyConAppOK ev tc1 tys1 tys2 +canDecomposableTyConAppOK ev eq_rel tc tys1 tys2 = case ev of CtDerived { ctev_loc = loc } - -> mapM_ (unifyDerived loc) (zipWith Pair tys1 tys2) + -> unifyDeriveds loc tc_roles tys1 tys2 CtWanted { ctev_evar = evar, ctev_loc = loc } - -> do { cos <- zipWithM (unifyWanted loc) tys1 tys2 - ; setEvBind evar (EvCoercion (mkTcTyConAppCo Nominal tc1 cos)) } + -> do { cos <- zipWith3M (unifyWanted loc) tc_roles tys1 tys2 + ; setEvBind evar (EvCoercion (mkTcTyConAppCo role tc cos)) } CtGiven { ctev_evtm = ev_tm, ctev_loc = loc } - -> do { given_evs <- newGivenEvVars loc $ - zipWith3 (mk_given ev_tm) tys1 tys2 [0..] + -> do { let ev_co = evTermCoercion ev_tm + ; given_evs <- newGivenEvVars loc $ + [ ( mkTcEqPredRole r ty1 ty2 + , EvCoercion (mkTcNthCo i ev_co) ) + | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..] + , r /= Phantom ] ; emitWorkNC given_evs } where - mk_given ev_tm ty1 ty2 i - = (mkTcEqPred ty1 ty2, EvCoercion (mkTcNthCo i (evTermCoercion ev_tm))) - --------------------- -canEqFailure :: CtEvidence -> TcType -> TcType -> TcS (StopOrContinue Ct) + role = eqRelRole eq_rel + tc_roles = tyConRolesX role tc + +-- | Call when canonicalizing an equality fails, but if the equality is +-- representational, there is some hope for the future. +-- Examples in Note [Flatten irreducible representational equalities] +canEqFailure :: CtEvidence -> EqRel + -> TcType -> TcType -> TcS (StopOrContinue Ct) +canEqFailure ev ReprEq ty1 ty2 + = do { -- See Note [Flatten irreducible representational equalities] + (xi1, co1) <- flatten FM_FlattenAll ev ty1 + ; (xi2, co2) <- flatten FM_FlattenAll ev ty2 + ; traceTcS "canEqFailure with ReprEq" $ + vcat [ ppr ev, ppr ty1, ppr ty2, ppr xi1, ppr xi2 ] + ; if xi1 `eqType` ty1 && xi2 `eqType` ty2 + then continueWith (CIrredEvCan { cc_ev = ev }) -- co1/2 must be refl + else rewriteEqEvidence ev ReprEq NotSwapped xi1 xi2 co1 co2 + `andWhenContinue` \ new_ev -> + can_eq_nc new_ev ReprEq xi1 xi1 xi2 xi2 } +canEqFailure ev NomEq ty1 ty2 = canEqHardFailure ev NomEq ty1 ty2 + +-- | Call when canonicalizing an equality fails with utterly no hope. +canEqHardFailure :: CtEvidence -> EqRel + -> TcType -> TcType -> TcS (StopOrContinue Ct) -- See Note [Make sure that insolubles are fully rewritten] -canEqFailure ev ty1 ty2 +canEqHardFailure ev eq_rel ty1 ty2 = do { (s1, co1) <- flatten FM_SubstOnly ev ty1 ; (s2, co2) <- flatten FM_SubstOnly ev ty2 - ; mb_ct <- rewriteEqEvidence ev NotSwapped s1 s2 co1 co2 - ; case mb_ct of - ContinueWith new_ev -> do { emitInsoluble (mkNonCanonical new_ev) - ; stopWith new_ev "Definitely not equal" } - Stop ev s -> pprPanic "canEqFailure" (s $$ ppr ev $$ ppr ty1 $$ ppr ty2) } + ; rewriteEqEvidence ev eq_rel NotSwapped s1 s2 co1 co2 + `andWhenContinue` \ new_ev -> + do { emitInsoluble (mkNonCanonical new_ev) + ; stopWith new_ev "Definitely not equal" }} {- +Note [Flatten irreducible representational equalities] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When we can't make any progress with a representational equality, but +we haven't given up all hope, we must flatten before producing the +CIrredEvCan. There are two reasons to do this: + + * See case in Note [Use canEqFailure in canDecomposableTyConApp]. + Flattening here can expose that we know enough information to unwrap + a newtype. + + * This case, which was encountered in the testsuite (T9117_3): + + work item: [W] c1: f a ~R g a + inert set: [G] c2: g ~R f + + In can_eq_app, we try to flatten the LHS of c1. This causes no effect, + because `f` cannot be rewritten. So, we go to can_eq_flat_app. Without + flattening the RHS, the reflexivity check fails, and we give up. However, + flattening the RHS rewrites `g` to `f`, the reflexivity check succeeds, + and we go on to glory. + Note [Decomposing TyConApps] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ If we see (T s1 t1 ~ T s2 t2), then we can just decompose to @@ -604,7 +805,6 @@ and we get just Refl. So canDecomposableTyCon is a fast-path decomposition that uses unifyWanted etc to short-cut that work. - Note [Canonicalising type applications] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Given (s1 t1) ~ ty2, how should we proceed? @@ -659,6 +859,28 @@ As this point we have an insoluble constraint, like Int~Bool. case we don't want to get two (or more) error messages by generating two (or more) insoluble fundep constraints from the same class constraint. + +Note [No top-level newtypes on RHS of representational equalities] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we're in this situation: + + work item: [W] c1 : a ~R b + inert: [G] c2 : b ~R Id a + +where + newtype Id a = Id a + +Further, suppose flattening `a` doesn't do anything. Then, we'll flatten the +RHS of c1 and have a new [W] c3 : a ~R Id a. If we just blindly proceed, we'll +fail in canEqTyVar2 with an occurs-check. What we really need to do is to +unwrap the `Id a` in the RHS. This is exactly analogous to the requirement for +no top-level type families on the RHS of a nominal equality. The only +annoyance is that the flattener doesn't do this work for us when flattening +the RHS, so we have to catch this case here and then go back to the beginning +of can_eq_nc. We know that this can't loop forever because we require that +flattening the RHS actually made progress. (If it didn't, then we really +*should* fail with an occurs-check!) + -} canCFunEqCan :: CtEvidence @@ -670,52 +892,68 @@ canCFunEqCan :: CtEvidence -- and the RHS is a fsk, which we must *not* substitute. -- So just substitute in the LHS canCFunEqCan ev fn tys fsk - = do { (tys', cos) <- flattenMany FM_FlattenAll ev tys + = do { (tys', cos) <- flattenMany FM_FlattenAll ev (repeat Nominal) tys -- cos :: tys' ~ tys ; let lhs_co = mkTcTyConAppCo Nominal fn cos -- :: F tys' ~ F tys new_lhs = mkTyConApp fn tys' fsk_ty = mkTyVarTy fsk - ; mb_ev <- rewriteEqEvidence ev NotSwapped new_lhs fsk_ty - lhs_co (mkTcNomReflCo fsk_ty) - ; case mb_ev of { - Stop ev s -> return (Stop ev s) ; - ContinueWith ev' -> - - do { extendFlatCache fn tys' (ctEvCoercion ev', fsk_ty, ev') + ; rewriteEqEvidence ev NomEq NotSwapped new_lhs fsk_ty + lhs_co (mkTcNomReflCo fsk_ty) + `andWhenContinue` \ ev' -> + do { extendFlatCache fn tys' (ctEvCoercion ev', fsk_ty, ctEvFlavour ev') ; continueWith (CFunEqCan { cc_ev = ev', cc_fun = fn - , cc_tyargs = tys', cc_fsk = fsk }) } } } + , cc_tyargs = tys', cc_fsk = fsk }) } } --------------------- -canEqTyVar :: CtEvidence -> SwapFlag +canEqTyVar :: CtEvidence -> EqRel -> SwapFlag -> TcTyVar -> TcType -> TcType -> TcS (StopOrContinue Ct) -- A TyVar on LHS, but so far un-zonked -canEqTyVar ev swapped tv1 ty2 ps_ty2 -- ev :: tv ~ s2 +canEqTyVar ev eq_rel swapped tv1 ty2 ps_ty2 -- ev :: tv ~ s2 = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr ty2 $$ ppr swapped) - ; mb_yes <- flattenTyVarOuter ev tv1 + ; let fmode = mkFlattenEnv FM_FlattenAll ev -- the FM_ param is ignored + ; mb_yes <- flattenTyVarOuter fmode tv1 ; case mb_yes of - Right (ty1, co1) -- co1 :: ty1 ~ tv1 - -> do { mb <- rewriteEqEvidence ev swapped ty1 ps_ty2 - co1 (mkTcNomReflCo ps_ty2) - ; traceTcS "canEqTyVar2" (vcat [ppr tv1, ppr ty2, ppr swapped, ppr ty1, - ppUnless (isDerived ev) (ppr co1)]) - ; case mb of - Stop ev s -> return (Stop ev s) - ContinueWith new_ev -> can_eq_nc new_ev ty1 ty1 ty2 ps_ty2 } - - Left tv1' -> do { -- FM_Avoid commented out: see Note [Lazy flattening] in TcFlatten - -- let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True } - -- Flatten the RHS less vigorously, to avoid gratuitous flattening - -- True <=> xi2 should not itself be a type-function application - ; (xi2, co2) <- flatten FM_FlattenAll ev ps_ty2 -- co2 :: xi2 ~ ps_ty2 - -- Use ps_ty2 to preserve type synonyms if poss - ; dflags <- getDynFlags - ; canEqTyVar2 dflags ev swapped tv1' xi2 co2 } } + { Right (ty1, co1) -> -- co1 :: ty1 ~ tv1 + do { traceTcS "canEqTyVar2" + (vcat [ ppr tv1, ppr ty2, ppr swapped + , ppr ty1 , ppUnless (isDerived ev) (ppr co1)]) + ; rewriteEqEvidence ev eq_rel swapped ty1 ps_ty2 + co1 (mkTcReflCo (eqRelRole eq_rel) ps_ty2) + `andWhenContinue` \ new_ev -> + can_eq_nc new_ev eq_rel ty1 ty1 ty2 ps_ty2 } + + ; Left tv1' -> + do { -- FM_Avoid commented out: see Note [Lazy flattening] in TcFlatten + -- let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True } + -- Flatten the RHS less vigorously, to avoid gratuitous flattening + -- True <=> xi2 should not itself be a type-function application + ; (xi2, co2) <- flatten FM_FlattenAll ev ps_ty2 -- co2 :: xi2 ~ ps_ty2 + -- Use ps_ty2 to preserve type synonyms if poss + ; traceTcS "canEqTyVar flat LHS" + (vcat [ ppr tv1, ppr tv1', ppr ty2, ppr swapped, ppr xi2 ]) + ; dflags <- getDynFlags + ; case eq_rel of + -- See Note [No top-level newtypes on RHS of representational equalities] + ReprEq + | Just (tc2, _) <- tcSplitTyConApp_maybe xi2 + , isNewTyCon tc2 + , not (ps_ty2 `eqType` xi2) + -> do { let xi1 = mkTyVarTy tv1' + role = eqRelRole eq_rel + ; traceTcS "canEqTyVar exposed newtype" + (vcat [ ppr tv1', ppr ps_ty2, ppr xi2, ppr tc2 ]) + ; rewriteEqEvidence ev eq_rel swapped xi1 xi2 + (mkTcReflCo role xi1) co2 + `andWhenContinue` \ new_ev -> + can_eq_nc new_ev eq_rel xi1 xi1 xi2 xi2 } + _ -> canEqTyVar2 dflags ev eq_rel swapped tv1' xi2 co2 } } } canEqTyVar2 :: DynFlags -> CtEvidence -- olhs ~ orhs (or, if swapped, orhs ~ olhs) + -> EqRel -> SwapFlag -> TcTyVar -- olhs -> TcType -- nrhs @@ -725,46 +963,54 @@ canEqTyVar2 :: DynFlags -- and RHS is fully rewritten, but with type synonyms -- preserved as much as possible -canEqTyVar2 dflags ev swapped tv1 xi2 co2 +canEqTyVar2 dflags ev eq_rel swapped tv1 xi2 co2 | Just tv2 <- getTyVar_maybe xi2 - = canEqTyVarTyVar ev swapped tv1 tv2 co2 + = canEqTyVarTyVar ev eq_rel swapped tv1 tv2 co2 | OC_OK xi2' <- occurCheckExpand dflags tv1 xi2 -- No occurs check - = do { mb <- rewriteEqEvidence ev swapped xi1 xi2' co1 co2 + = do { let k1 = tyVarKind tv1 + k2 = typeKind xi2' + ; rewriteEqEvidence ev eq_rel swapped xi1 xi2' co1 co2 -- Ensure that the new goal has enough type synonyms -- expanded by the occurCheckExpand; hence using xi2' here -- See Note [occurCheckExpand] - - ; let k1 = tyVarKind tv1 - k2 = typeKind xi2' - ; case mb of - Stop ev s -> return (Stop ev s) - ContinueWith new_ev - | k2 `isSubKind` k1 - -- Establish CTyEqCan kind invariant + `andWhenContinue` \ new_ev -> + if k2 `isSubKind` k1 + then -- Establish CTyEqCan kind invariant -- Reorientation has done its best, but the kinds might -- simply be incompatible - -> continueWith (CTyEqCan { cc_ev = new_ev - , cc_tyvar = tv1, cc_rhs = xi2' }) - | otherwise - -> incompatibleKind new_ev xi1 k1 xi2' k2 } + continueWith (CTyEqCan { cc_ev = new_ev + , cc_tyvar = tv1, cc_rhs = xi2' + , cc_eq_rel = eq_rel }) + else incompatibleKind new_ev xi1 k1 xi2' k2 } | otherwise -- Occurs check error - = do { mb <- rewriteEqEvidence ev swapped xi1 xi2 co1 co2 - ; case mb of - Stop ev s -> return (Stop ev s) - ContinueWith new_ev -> do { emitInsoluble (mkNonCanonical new_ev) + = rewriteEqEvidence ev eq_rel swapped xi1 xi2 co1 co2 + `andWhenContinue` \ new_ev -> + case eq_rel of + NomEq -> do { emitInsoluble (mkNonCanonical new_ev) -- If we have a ~ [a], it is not canonical, and in particular -- we don't want to rewrite existing inerts with it, otherwise -- we'd risk divergence in the constraint solver - ; stopWith new_ev "Occurs check" } } + ; stopWith new_ev "Occurs check" } + + -- A representational equality with an occurs-check problem isn't + -- insoluble! For example: + -- a ~R b a + -- We might learn that b is the newtype Id. + -- But, the occurs-check certainly prevents the equality from being + -- canonical, and we might loop if we were to use it in rewriting. + ReprEq -> do { traceTcS "Occurs-check in representational equality" + (ppr xi1 $$ ppr xi2) + ; continueWith (CIrredEvCan { cc_ev = new_ev }) } where xi1 = mkTyVarTy tv1 - co1 = mkTcNomReflCo xi1 + co1 = mkTcReflCo (eqRelRole eq_rel) xi1 canEqTyVarTyVar :: CtEvidence -- tv1 ~ orhs (or orhs ~ tv1, if swapped) + -> EqRel -> SwapFlag -> TcTyVar -> TcTyVar -- tv2, tv2 -> TcCoercion -- tv2 ~ orhs @@ -774,10 +1020,10 @@ canEqTyVarTyVar :: CtEvidence -- tv1 ~ orhs (or orhs ~ tv1, if swapped -- rw_orhs = tv1, rw_olhs = orhs -- rw_nlhs = tv2, rw_nrhs = xi1 -- See Note [Canonical orientation for tyvar/tyvar equality constraints] -canEqTyVarTyVar ev swapped tv1 tv2 co2 +canEqTyVarTyVar ev eq_rel swapped tv1 tv2 co2 | tv1 == tv2 = do { when (isWanted ev) $ - ASSERT( tcCoercionRole co2 == Nominal ) + ASSERT( tcCoercionRole co2 == eqRelRole eq_rel ) setEvBind (ctev_evar ev) (EvCoercion (maybeSym swapped co2)) ; stopWith ev "Equal tyvars" } @@ -792,7 +1038,7 @@ canEqTyVarTyVar ev swapped tv1 tv2 co2 xi2 = mkTyVarTy tv2 k1 = tyVarKind tv1 k2 = tyVarKind tv2 - co1 = mkTcNomReflCo xi1 + co1 = mkTcReflCo (eqRelRole eq_rel) xi1 k1_sub_k2 = k1 `isSubKind` k2 k2_sub_k1 = k2 `isSubKind` k1 same_kind = k1_sub_k2 && k2_sub_k1 @@ -805,8 +1051,9 @@ canEqTyVarTyVar ev swapped tv1 tv2 co2 -- ev : tv1 ~ orhs (not swapped) or orhs ~ tv1 (swapped) -- co1 : xi1 ~ tv1 -- co2 : xi2 ~ tv2 - = do { mb <- rewriteEqEvidence ev swapped xi1 xi2 co1 co2 - ; let mk_ct ev' = CTyEqCan { cc_ev = ev', cc_tyvar = tv1, cc_rhs = xi2 } + = do { mb <- rewriteEqEvidence ev eq_rel swapped xi1 xi2 co1 co2 + ; let mk_ct ev' = CTyEqCan { cc_ev = ev', cc_tyvar = tv1 + , cc_rhs = xi2 , cc_eq_rel = eq_rel } ; return (fmap mk_ct mb) } -- See Note [Orient equalities with flatten-meta-vars on the left] in TcFlatten @@ -817,15 +1064,16 @@ canEqTyVarTyVar ev swapped tv1 tv2 co2 = ASSERT2( k1_sub_k2, ppr tv1 $$ ppr tv2 ) ASSERT2( isWanted ev, ppr ev ) -- Only wanteds have flatten meta-vars do { tv_ty <- newFlexiTcSTy (tyVarKind tv1) - ; new_ev <- newWantedEvVarNC (ctEvLoc ev) (mkTcEqPred tv_ty xi2) + ; new_ev <- newWantedEvVarNC (ctEvLoc ev) + (mkTcEqPredRole (eqRelRole eq_rel) + tv_ty xi2) ; emitWorkNC [new_ev] ; canon_eq swapped tv1 xi1 tv_ty co1 (ctEvCoercion new_ev `mkTcTransCo` co2) } incompat - = do { mb <- rewriteEqEvidence ev swapped xi1 xi2 (mkTcNomReflCo xi1) co2 - ; case mb of - Stop ev s -> return (Stop ev s) - ContinueWith ev' -> incompatibleKind ev' xi1 k1 xi2 k2 } + = rewriteEqEvidence ev eq_rel swapped xi1 xi2 (mkTcNomReflCo xi1) co2 + `andWhenContinue` \ ev' -> + incompatibleKind ev' xi1 k1 xi2 k2 swap_over -- If tv1 is touchable, swap only if tv2 is also @@ -856,6 +1104,17 @@ canEqTyVarTyVar ev swapped tv1 tv2 co2 = (isSigTyVar tv1 && not (isSigTyVar tv2)) || (isSystemName (Var.varName tv2) && not (isSystemName (Var.varName tv1))) +-- | Solve a reflexive equality constraint +canEqReflexive :: CtEvidence -- ty ~ ty + -> EqRel + -> TcType -- ty + -> TcS (StopOrContinue Ct) -- always Stop +canEqReflexive ev eq_rel ty + = do { when (isWanted ev) $ + setEvBind (ctev_evar ev) (EvCoercion $ + mkTcReflCo (eqRelRole eq_rel) ty) + ; stopWith ev "Solved by reflexivity" } + incompatibleKind :: CtEvidence -- t1~t2 -> TcType -> TcKind -> TcType -> TcKind -- s1~s2, flattened and zonked @@ -1161,6 +1420,7 @@ andWhenContinue tcs1 tcs2 ; case r of Stop ev s -> return (Stop ev s) ContinueWith ct -> tcs2 ct } +infixr 0 `andWhenContinue` -- allow chaining with ($) rewriteEvidence :: CtEvidence -- old evidence -> TcPredType -- new predicate @@ -1217,16 +1477,20 @@ rewriteEvidence old_ev new_pred co | isTcReflCo co -- See Note [Rewriting with Refl] = return (ContinueWith (old_ev { ctev_pred = new_pred })) -rewriteEvidence (CtGiven { ctev_evtm = old_tm , ctev_loc = loc }) new_pred co +rewriteEvidence ev@(CtGiven { ctev_evtm = old_tm , ctev_loc = loc }) new_pred co = do { new_ev <- newGivenEvVar loc (new_pred, new_tm) -- See Note [Bind new Givens immediately] ; return (ContinueWith new_ev) } where - new_tm = mkEvCast old_tm (mkTcSubCo (mkTcSymCo co)) -- mkEvCast optimises ReflCo + -- mkEvCast optimises ReflCo + new_tm = mkEvCast old_tm (tcDowngradeRole Representational + (ctEvRole ev) + (mkTcSymCo co)) rewriteEvidence ev@(CtWanted { ctev_evar = evar, ctev_loc = loc }) new_pred co = do { (new_ev, freshness) <- newWantedEvVar loc new_pred - ; MASSERT( tcCoercionRole co == Nominal ) - ; setEvBind evar (mkEvCast (ctEvTerm new_ev) (mkTcSubCo co)) + ; MASSERT( tcCoercionRole co == ctEvRole ev ) + ; setEvBind evar (mkEvCast (ctEvTerm new_ev) + (tcDowngradeRole Representational (ctEvRole ev) co)) ; case freshness of Fresh -> continueWith new_ev Cached -> stopWith ev "Cached wanted" } @@ -1234,6 +1498,7 @@ rewriteEvidence ev@(CtWanted { ctev_evar = evar, ctev_loc = loc }) new_pred co rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swapped) -- or orhs ~ olhs (swapped) + -> EqRel -> SwapFlag -> TcType -> TcType -- New predicate nlhs ~ nrhs -- Should be zonked, because we use typeKind on nlhs/nrhs @@ -1255,9 +1520,9 @@ rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swap -- w : orhs ~ olhs = sym rhs_co ; sym w1 ; lhs_co -- -- It's all a form of rewwriteEvidence, specialised for equalities -rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co - | CtDerived { ctev_loc = loc } <- old_ev - = do { mb <- newDerived loc new_pred +rewriteEqEvidence old_ev eq_rel swapped nlhs nrhs lhs_co rhs_co + | CtDerived {} <- old_ev + = do { mb <- newDerived loc' new_pred ; case mb of Just new_ev -> continueWith new_ev Nothing -> stopWith old_ev "Cached derived" } @@ -1267,15 +1532,16 @@ rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co , isTcReflCo rhs_co = return (ContinueWith (old_ev { ctev_pred = new_pred })) - | CtGiven { ctev_evtm = old_tm , ctev_loc = loc } <- old_ev + | CtGiven { ctev_evtm = old_tm } <- old_ev = do { let new_tm = EvCoercion (lhs_co `mkTcTransCo` maybeSym swapped (evTermCoercion old_tm) `mkTcTransCo` mkTcSymCo rhs_co) - ; new_ev <- newGivenEvVar loc (new_pred, new_tm) -- See Note [Bind new Givens immediately] + ; new_ev <- newGivenEvVar loc' (new_pred, new_tm) + -- See Note [Bind new Givens immediately] ; return (ContinueWith new_ev) } - | CtWanted { ctev_evar = evar, ctev_loc = loc } <- old_ev - = do { new_evar <- newWantedEvVarNC loc new_pred + | CtWanted { ctev_evar = evar } <- old_ev + = do { new_evar <- newWantedEvVarNC loc' new_pred ; let co = maybeSym swapped $ mkTcSymCo lhs_co `mkTcTransCo` ctEvCoercion new_evar @@ -1287,7 +1553,13 @@ rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co | otherwise = panic "rewriteEvidence" where - new_pred = mkTcEqPred nlhs nrhs + new_pred = mkTcEqPredRole (eqRelRole eq_rel) nlhs nrhs + + -- equality is like a type class. Bumping the depth is necessary because + -- of recursive newtypes, where "reducing" a newtype can actually make + -- it bigger. See Note [Eager reflexivity check] in TcCanonical before + -- considering changing this behavior. + loc' = bumpCtLocDepth CountConstraints (ctEvLoc old_ev) {- Note [unifyWanted and unifyDerived] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1302,25 +1574,29 @@ But where it succeeds in finding common structure, it just builds a coercion to reflect it. -} -unifyWanted :: CtLoc -> TcType -> TcType -> TcS TcCoercion +unifyWanted :: CtLoc -> Role -> TcType -> TcType -> TcS TcCoercion -- Return coercion witnessing the equality of the two types, -- emitting new work equalities where necessary to achieve that -- Very good short-cut when the two types are equal, or nearly so -- See Note [unifyWanted and unifyDerived] -unifyWanted loc orig_ty1 orig_ty2 +-- The returned coercion's role matches the input parameter +unifyWanted _ Phantom ty1 ty2 = return (mkTcPhantomCo ty1 ty2) +unifyWanted loc role orig_ty1 orig_ty2 = go orig_ty1 orig_ty2 where 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) - = do { co_s <- unifyWanted loc s1 s2 - ; co_t <- unifyWanted loc t1 t2 - ; return (mkTcTyConAppCo Nominal funTyCon [co_s,co_t]) } + = do { co_s <- unifyWanted loc role s1 s2 + ; co_t <- unifyWanted loc role t1 t2 + ; return (mkTcTyConAppCo role funTyCon [co_s,co_t]) } go (TyConApp tc1 tys1) (TyConApp tc2 tys2) | tc1 == tc2, isDecomposableTyCon tc1, tys1 `equalLength` tys2 - = do { cos <- zipWithM (unifyWanted loc) tys1 tys2 - ; return (mkTcTyConAppCo Nominal tc1 cos) } + , (not (isNewTyCon tc1) && not (isDataFamilyTyCon tc1)) || role == Nominal + -- don't look under newtypes! + = do { cos <- zipWith3M (unifyWanted loc) (tyConRolesX role tc1) tys1 tys2 + ; return (mkTcTyConAppCo role tc1 cos) } go (TyVarTy tv) ty2 = do { mb_ty <- isFilledMetaTyVar_maybe tv ; case mb_ty of @@ -1333,34 +1609,37 @@ unifyWanted loc orig_ty1 orig_ty2 Nothing -> bale_out } go _ _ = bale_out - bale_out = do { ev <- newWantedEvVarNC loc (mkTcEqPred orig_ty1 orig_ty2) + bale_out = do { ev <- newWantedEvVarNC loc (mkTcEqPredRole role + orig_ty1 orig_ty2) ; emitWorkNC [ev] ; return (ctEvCoercion ev) } -unifyDeriveds :: CtLoc -> [TcType] -> [TcType] -> TcS () +unifyDeriveds :: CtLoc -> [Role] -> [TcType] -> [TcType] -> TcS () -- See Note [unifyWanted and unifyDerived] -unifyDeriveds loc tys1 tys2 = zipWithM_ (unify_derived loc) tys1 tys2 +unifyDeriveds loc roles tys1 tys2 = zipWith3M_ (unify_derived loc) roles tys1 tys2 -unifyDerived :: CtLoc -> Pair TcType -> TcS () +unifyDerived :: CtLoc -> Role -> Pair TcType -> TcS () -- See Note [unifyWanted and unifyDerived] -unifyDerived loc (Pair ty1 ty2) = unify_derived loc ty1 ty2 +unifyDerived loc role (Pair ty1 ty2) = unify_derived loc role ty1 ty2 -unify_derived :: CtLoc -> TcType -> TcType -> TcS () +unify_derived :: CtLoc -> Role -> TcType -> TcType -> TcS () -- Create new Derived and put it in the work list -- Should do nothing if the two types are equal -- See Note [unifyWanted and unifyDerived] -unify_derived loc orig_ty1 orig_ty2 +unify_derived _ Phantom _ _ = return () +unify_derived loc role orig_ty1 orig_ty2 = go orig_ty1 orig_ty2 where 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) - = do { unify_derived loc s1 s2 - ; unify_derived loc t1 t2 } + = do { unify_derived loc role s1 s2 + ; unify_derived loc role t1 t2 } go (TyConApp tc1 tys1) (TyConApp tc2 tys2) | tc1 == tc2, isDecomposableTyCon tc1, tys1 `equalLength` tys2 - = unifyDeriveds loc tys1 tys2 + , (not (isNewTyCon tc1) && not (isDataFamilyTyCon tc1)) || role == Nominal + = unifyDeriveds loc (tyConRolesX role tc1) tys1 tys2 go (TyVarTy tv) ty2 = do { mb_ty <- isFilledMetaTyVar_maybe tv ; case mb_ty of @@ -1373,7 +1652,7 @@ unify_derived loc orig_ty1 orig_ty2 Nothing -> bale_out } go _ _ = bale_out - bale_out = emitNewDerived loc (mkTcEqPred orig_ty1 orig_ty2) + bale_out = emitNewDerived loc (mkTcEqPredRole role orig_ty1 orig_ty2) maybeSym :: SwapFlag -> TcCoercion -> TcCoercion maybeSym IsSwapped co = mkTcSymCo co diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs index 457720708f..3d3eb5075a 100644 --- a/compiler/typecheck/TcDeriv.hs +++ b/compiler/typecheck/TcDeriv.hs @@ -1807,7 +1807,6 @@ inferInstanceContexts infer_specs do { theta <- simplifyDeriv the_pred tyvars deriv_rhs -- checkValidInstance tyvars theta clas inst_tys -- Not necessary; see Note [Exotic derived instance contexts] - -- in TcSimplify ; traceTc "TcDeriv" (ppr deriv_rhs $$ ppr theta) -- Claim: the result instance declaration is guaranteed valid diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index 56c33b15fe..f993f60bb5 100644 --- a/compiler/typecheck/TcErrors.hs +++ b/compiler/typecheck/TcErrors.hs @@ -18,19 +18,19 @@ import Type import Kind ( isKind ) import Unify ( tcMatchTys ) import Module -import FamInst ( FamInstEnvs, tcGetFamInstEnvs, tcLookupDataFamInst ) +import FamInst import Inst import InstEnv import TyCon import DataCon import TcEvidence -import TysWiredIn ( coercibleClass ) import Name -import RdrName ( lookupGRE_Name ) +import RdrName ( lookupGRE_Name, GlobalRdrEnv ) import Id import Var import VarSet import VarEnv +import NameEnv import Bag import ErrUtils ( ErrMsg, makeIntoWarning, pprLocErrMsg, isWarning ) import BasicTypes @@ -44,7 +44,7 @@ import ListSetOps ( equivClasses ) import Control.Monad ( when ) import Data.Maybe -import Data.List ( partition, mapAccumL, zip4, nub, sortBy ) +import Data.List ( partition, mapAccumL, nub, sortBy ) {- ************************************************************************ @@ -277,12 +277,12 @@ reportFlats ctxt flats -- Here 'flats' includes insolble goals utterly_wrong, skolem_eq, is_hole, is_dict, is_equality, is_ip, is_irred :: Ct -> PredTree -> Bool - utterly_wrong _ (EqPred ty1 ty2) = isRigid ty1 && isRigid ty2 + utterly_wrong _ (EqPred _ ty1 ty2) = isRigid ty1 && isRigid ty2 utterly_wrong _ _ = False is_hole ct _ = isHoleCt ct - skolem_eq _ (EqPred ty1 ty2) = isRigidOrSkol ty1 && isRigidOrSkol ty2 + skolem_eq _ (EqPred NomEq ty1 ty2) = isRigidOrSkol ty1 && isRigidOrSkol ty2 skolem_eq _ _ = False is_equality _ (EqPred {}) = True @@ -340,7 +340,8 @@ mkSkolReporter ctxt cts where cmp_lhs_type ct1 ct2 = case (classifyPredType (ctPred ct1), classifyPredType (ctPred ct2)) of - (EqPred ty1 _, EqPred ty2 _) -> ty1 `cmpType` ty2 + (EqPred eq_rel1 ty1 _, EqPred eq_rel2 ty2 _) -> + (eq_rel1 `compare` eq_rel2) `thenCmp` (ty1 `cmpType` ty2) _ -> pprPanic "mkSkolReporter" (ppr ct1 $$ ppr ct2) mkHoleReporter :: (ReportErrCtxt -> Ct -> TcM ErrMsg) -> Reporter @@ -666,11 +667,16 @@ mkEqErr1 ctxt ct | otherwise -- Wanted or derived = do { (ctxt, binds_msg) <- relevantBindings True ctxt ct ; (env1, tidy_orig) <- zonkTidyOrigin (cec_tidy ctxt) (ctLocOrigin loc) + ; rdr_env <- getGlobalRdrEnv + ; fam_envs <- tcGetFamInstEnvs ; let (is_oriented, wanted_msg) = mk_wanted_extra tidy_orig + coercible_msg = case ctEvEqRel ev of + NomEq -> empty + ReprEq -> mkCoercibleExplanation rdr_env fam_envs ty1 ty2 ; dflags <- getDynFlags ; traceTc "mkEqErr1" (ppr ct $$ pprCtOrigin (ctLocOrigin loc) $$ pprCtOrigin tidy_orig) ; mkEqErr_help dflags (ctxt {cec_tidy = env1}) - (wanted_msg $$ binds_msg) + (wanted_msg $$ coercible_msg $$ binds_msg) ct is_oriented ty1 ty2 } where ev = ctEvidence ct @@ -700,9 +706,86 @@ mkEqErr1 ctxt ct TypeEqOrigin {} -> snd (mkExpectedActualMsg cty1 cty2 sub_o) _ -> empty - mk_wanted_extra orig@(FunDepOrigin1 {}) = (Nothing, pprArising orig) - mk_wanted_extra orig@(FunDepOrigin2 {}) = (Nothing, pprArising orig) - mk_wanted_extra _ = (Nothing, empty) + mk_wanted_extra orig@(FunDepOrigin1 {}) = (Nothing, pprArising orig) + mk_wanted_extra orig@(FunDepOrigin2 {}) = (Nothing, pprArising orig) + mk_wanted_extra orig@(DerivOriginCoerce _ oty1 oty2) + = (Nothing, pprArising orig $+$ mkRoleSigs oty1 oty2) + mk_wanted_extra orig@(CoercibleOrigin oty1 oty2) + -- if the origin types are the same as the final types, don't + -- clutter output with repetitive information + | not (oty1 `eqType` ty1 && oty2 `eqType` ty2) && + not (oty1 `eqType` ty2 && oty2 `eqType` ty1) + = (Nothing, pprArising orig $+$ mkRoleSigs oty1 oty2) + | otherwise + -- still print role sigs even if types line up + = (Nothing, mkRoleSigs oty1 oty2) + mk_wanted_extra _ = (Nothing, empty) + +-- | This function tries to reconstruct why a "Coercible ty1 ty2" constraint +-- is left over. +mkCoercibleExplanation :: GlobalRdrEnv -> FamInstEnvs + -> TcType -> TcType -> SDoc +mkCoercibleExplanation rdr_env fam_envs ty1 ty2 + | Just (tc, tys) <- tcSplitTyConApp_maybe ty1 + , (rep_tc, _, _) <- tcLookupDataFamInst fam_envs tc tys + , Just msg <- coercible_msg_for_tycon rep_tc + = msg + | Just (tc, tys) <- splitTyConApp_maybe ty2 + , (rep_tc, _, _) <- tcLookupDataFamInst fam_envs tc tys + , Just msg <- coercible_msg_for_tycon rep_tc + = msg + | Just (s1, _) <- tcSplitAppTy_maybe ty1 + , Just (s2, _) <- tcSplitAppTy_maybe ty2 + , s1 `eqType` s2 + , has_unknown_roles s1 + = hang (text "NB: We cannot know what roles the parameters to" <+> + quotes (ppr s1) <+> text "have;") + 2 (text "we must assume that the role is nominal") + | otherwise + = empty + where + coercible_msg_for_tycon tc + | isAbstractTyCon tc + = Just $ hsep [ text "NB: The type constructor" + , quotes (pprSourceTyCon tc) + , text "is abstract" ] + | isNewTyCon tc + , [data_con] <- tyConDataCons tc + , let dc_name = dataConName data_con + , null (lookupGRE_Name rdr_env dc_name) + = Just $ hang (text "The data constructor" <+> quotes (ppr dc_name)) + 2 (sep [ text "of newtype" <+> quotes (pprSourceTyCon tc) + , text "is not in scope" ]) + | otherwise = Nothing + + has_unknown_roles ty + | Just (tc, tys) <- tcSplitTyConApp_maybe ty + = length tys >= tyConArity tc -- oversaturated tycon + | Just (s, _) <- tcSplitAppTy_maybe ty + = has_unknown_roles s + | isTyVarTy ty + = True + | otherwise + = False + +-- | Make a listing of role signatures for all the parameterised tycons +-- used in the provided types +mkRoleSigs :: Type -> Type -> SDoc +mkRoleSigs ty1 ty2 + = ppUnless (null role_sigs) $ + hang (text "Relevant role signatures:") + 2 (vcat role_sigs) + where + tcs = nameEnvElts $ tyConsOfType ty1 `plusNameEnv` tyConsOfType ty2 + role_sigs = mapMaybe ppr_role_sig tcs + + ppr_role_sig tc + | null roles -- if there are no parameters, don't bother printing + = Nothing + | otherwise + = Just $ hsep $ [text "type role", ppr tc] ++ map ppr roles + where + roles = tyConRoles tc mkEqErr_help :: DynFlags -> ReportErrCtxt -> SDoc -> Ct @@ -743,6 +826,7 @@ mkTyVarEqErr dflags ctxt extra ct oriented tv1 ty2 = mkErrorMsg ctxt ct $ (kindErrorMsg (mkTyVarTy tv1) ty2 $$ extra) | OC_Occurs <- occ_check_expand + , NomEq <- ctEqRel ct -- reporting occurs check for Coercible is strange = do { let occCheckMsg = hang (text "Occurs check: cannot construct the infinite type:") 2 (sep [ppr ty1, char '~', ppr ty2]) extra2 = mkEqInfoMsg ct ty1 ty2 @@ -762,7 +846,7 @@ mkTyVarEqErr dflags ctxt extra ct oriented tv1 ty2 | (implic:_) <- cec_encl ctxt , Implic { ic_skols = skols } <- implic , tv1 `elem` skols - = mkErrorMsg ctxt ct (vcat [ misMatchMsg oriented ty1 ty2 + = mkErrorMsg ctxt ct (vcat [ misMatchMsg oriented eq_rel ty1 ty2 , extraTyVarInfo ctxt tv1 ty2 , extra ]) @@ -771,7 +855,7 @@ mkTyVarEqErr dflags ctxt extra ct oriented tv1 ty2 , Implic { ic_env = env, ic_skols = skols, ic_info = skol_info } <- implic , let esc_skols = filter (`elemVarSet` (tyVarsOfType ty2)) skols , not (null esc_skols) - = do { let msg = misMatchMsg oriented ty1 ty2 + = do { let msg = misMatchMsg oriented eq_rel ty1 ty2 esc_doc = sep [ ptext (sLit "because type variable") <> plural esc_skols <+> pprQuotedList esc_skols , ptext (sLit "would escape") <+> @@ -789,7 +873,7 @@ mkTyVarEqErr dflags ctxt extra ct oriented tv1 ty2 -- Nastiest case: attempt to unify an untouchable variable | (implic:_) <- cec_encl ctxt -- Get the innermost context , Implic { ic_env = env, ic_given = given, ic_info = skol_info } <- implic - = do { let msg = misMatchMsg oriented ty1 ty2 + = do { let msg = misMatchMsg oriented eq_rel ty1 ty2 tclvl_extra = nest 2 $ sep [ quotes (ppr tv1) <+> ptext (sLit "is untouchable") @@ -807,9 +891,10 @@ mkTyVarEqErr dflags ctxt extra ct oriented tv1 ty2 -- Not an occurs check, because F is a type function. where occ_check_expand = occurCheckExpand dflags tv1 ty2 - k1 = tyVarKind tv1 - k2 = typeKind ty2 - ty1 = mkTyVarTy tv1 + k1 = tyVarKind tv1 + k2 = typeKind ty2 + ty1 = mkTyVarTy tv1 + eq_rel = ctEqRel ct mkEqInfoMsg :: Ct -> TcType -> TcType -> SDoc -- Report (a) ambiguity if either side is a type function application @@ -853,7 +938,7 @@ misMatchOrCND ctxt ct oriented ty1 ty2 isGivenCt ct -- If the equality is unconditionally insoluble -- or there is no context, don't report the context - = misMatchMsg oriented ty1 ty2 + = misMatchMsg oriented (ctEqRel ct) ty1 ty2 | otherwise = couldNotDeduce givens ([mkTcEqPred ty1 ty2], orig) where @@ -928,23 +1013,31 @@ kindErrorMsg ty1 ty2 k2 = typeKind ty2 -------------------- -misMatchMsg :: Maybe SwapFlag -> TcType -> TcType -> SDoc -- Types are already tidy +misMatchMsg :: Maybe SwapFlag -> EqRel -> TcType -> TcType -> SDoc +-- Types are already tidy -- If oriented then ty1 is actual, ty2 is expected -misMatchMsg oriented ty1 ty2 +misMatchMsg oriented eq_rel ty1 ty2 | Just IsSwapped <- oriented - = misMatchMsg (Just NotSwapped) ty2 ty1 + = misMatchMsg (Just NotSwapped) eq_rel ty2 ty1 | Just NotSwapped <- oriented - = sep [ ptext (sLit "Couldn't match expected") <+> what <+> quotes (ppr ty2) - , nest 12 $ ptext (sLit "with actual") <+> what <+> quotes (ppr ty1) + = sep [ text "Couldn't match" <+> repr1 <+> text "expected" <+> + what <+> quotes (ppr ty2) + , nest (12 + extra_space) $ + text "with" <+> repr2 <+> text "actual" <+> what <+> quotes (ppr ty1) , sameOccExtra ty2 ty1 ] | otherwise - = sep [ ptext (sLit "Couldn't match") <+> what <+> quotes (ppr ty1) - , nest 14 $ ptext (sLit "with") <+> quotes (ppr ty2) + = sep [ text "Couldn't match" <+> repr1 <+> what <+> quotes (ppr ty1) + , nest (15 + extra_space) $ + text "with" <+> repr2 <+> quotes (ppr ty2) , sameOccExtra ty1 ty2 ] where what | isKind ty1 = ptext (sLit "kind") | otherwise = ptext (sLit "type") + (repr1, repr2, extra_space) = case eq_rel of + NomEq -> (empty, empty, 0) + ReprEq -> (text "representation of", text "that of", 10) + mkExpectedActualMsg :: Type -> Type -> CtOrigin -> (Maybe SwapFlag, SDoc) -- NotSwapped means (actual, expected), IsSwapped is the reverse mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act, uo_expected = exp }) @@ -1048,7 +1141,6 @@ mkDictErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg mkDictErr ctxt cts = ASSERT( not (null cts) ) do { inst_envs <- tcGetInstEnvs - ; fam_envs <- tcGetFamInstEnvs ; let (ct1:_) = cts -- ct1 just for its location min_cts = elim_superclasses cts ; lookups <- mapM (lookup_cls_inst inst_envs) min_cts @@ -1059,7 +1151,7 @@ mkDictErr ctxt cts -- But we report only one of them (hence 'head') because they all -- have the same source-location origin, to try avoid a cascade -- of error from one location - ; (ctxt, err) <- mk_dict_err fam_envs ctxt (head (no_inst_cts ++ overlap_cts)) + ; (ctxt, err) <- mk_dict_err ctxt (head (no_inst_cts ++ overlap_cts)) ; mkErrorMsg ctxt ct1 err } where no_givens = null (getUserGivens ctxt) @@ -1085,17 +1177,16 @@ mkDictErr ctxt cts where min_preds = mkMinimalBySCs (map ctPred cts) -mk_dict_err :: FamInstEnvs -> ReportErrCtxt -> (Ct, ClsInstLookupResult) +mk_dict_err :: ReportErrCtxt -> (Ct, ClsInstLookupResult) -> TcM (ReportErrCtxt, SDoc) -- Report an overlap error if this class constraint results -- from an overlap (returning Left clas), otherwise return (Right pred) -mk_dict_err fam_envs ctxt (ct, (matches, unifiers, safe_haskell)) +mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell)) | null matches -- No matches but perhaps several unifiers = do { let (is_ambig, ambig_msg) = mkAmbigMsg ct ; (ctxt, binds_msg) <- relevantBindings True ctxt ct ; traceTc "mk_dict_err" (ppr ct $$ ppr is_ambig $$ ambig_msg) - ; rdr_env <- getGlobalRdrEnv - ; return (ctxt, cannot_resolve_msg rdr_env is_ambig binds_msg ambig_msg) } + ; return (ctxt, cannot_resolve_msg is_ambig binds_msg ambig_msg) } | not safe_haskell -- Some matches => overlap errors = return (ctxt, overlap_msg) @@ -1110,8 +1201,8 @@ mk_dict_err fam_envs ctxt (ct, (matches, unifiers, safe_haskell)) givens = getUserGivens ctxt all_tyvars = all isTyVarTy tys - cannot_resolve_msg rdr_env has_ambig_tvs binds_msg ambig_msg - = vcat [ addArising orig (no_inst_msg $$ coercible_explanation rdr_env) + cannot_resolve_msg has_ambig_tvs binds_msg ambig_msg + = vcat [ addArising orig no_inst_msg , vcat (pp_givens givens) , ppWhen (has_ambig_tvs && not (null unifiers && null givens)) (vcat [ ambig_msg, binds_msg, potential_msg ]) @@ -1143,11 +1234,6 @@ mk_dict_err fam_envs ctxt (ct, (matches, unifiers, safe_haskell)) ppr_skol skol_info = ppr skol_info no_inst_msg - | clas == coercibleClass - = let (ty1, ty2) = getEqPredTys pred - in sep [ ptext (sLit "Could not coerce from") <+> quotes (ppr ty1) - , nest 19 (ptext (sLit "to") <+> quotes (ppr ty2)) ] - -- The nesting makes the types line up | null givens && null matches = ptext (sLit "No instance for") <+> pprParendType pred @@ -1241,53 +1327,6 @@ mk_dict_err fam_envs ctxt (ct, (matches, unifiers, safe_haskell)) ] ] - -- This function tries to reconstruct why a "Coercible ty1 ty2" constraint - -- is left over. Therefore its logic has to stay in sync with - -- getCoericbleInst in TcInteract. See Note [Coercible Instances] - coercible_explanation rdr_env - | clas /= coercibleClass = empty - | Just (tc1,tyArgs1) <- splitTyConApp_maybe ty1, - Just (tc2,tyArgs2) <- splitTyConApp_maybe ty2, - tc1 == tc2 - = nest 2 $ vcat $ - [ fsep [ hsep [ ptext $ sLit "because the", speakNth n, ptext $ sLit "type argument"] - , hsep [ ptext $ sLit "of", quotes (ppr tc1), ptext $ sLit "has role Nominal,"] - , ptext $ sLit "but the arguments" - , quotes (ppr t1) - , ptext $ sLit "and" - , quotes (ppr t2) - , ptext $ sLit "differ" ] - | (n,Nominal,t1,t2) <- zip4 [1..] (tyConRoles tc1) tyArgs1 tyArgs2 - , not (t1 `eqType` t2) - ] - | Just (tc, tys) <- tcSplitTyConApp_maybe ty1 - , (rep_tc, _, _) <- tcLookupDataFamInst fam_envs tc tys - , Just msg <- coercible_msg_for_tycon rdr_env rep_tc - = msg - | Just (tc, tys) <- splitTyConApp_maybe ty2 - , (rep_tc, _, _) <- tcLookupDataFamInst fam_envs tc tys - , Just msg <- coercible_msg_for_tycon rdr_env rep_tc - = msg - | otherwise - = nest 2 $ sep [ ptext (sLit "because") <+> quotes (ppr ty1) - , nest 4 (vcat [ ptext (sLit "and") <+> quotes (ppr ty2) - , ptext (sLit "are different types.") ]) ] - where - (ty1, ty2) = getEqPredTys pred - - coercible_msg_for_tycon rdr_env tc - | isAbstractTyCon tc - = Just $ hsep [ ptext $ sLit "because the type constructor", quotes (pprSourceTyCon tc) - , ptext $ sLit "is abstract" ] - | isNewTyCon tc - , [data_con] <- tyConDataCons tc - , let dc_name = dataConName data_con - , null (lookupGRE_Name rdr_env dc_name) - = Just $ hang (ptext (sLit "because the data constructor") <+> quotes (ppr dc_name)) - 2 (sep [ ptext (sLit "of newtype") <+> quotes (pprSourceTyCon tc) - , ptext (sLit "is not in scope") ]) - | otherwise = Nothing - usefulContext :: ReportErrCtxt -> TcPredType -> [SkolemInfo] usefulContext ctxt pred = go (cec_encl ctxt) diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs index 5e4f4e8aa2..60ac88994e 100644 --- a/compiler/typecheck/TcEvidence.hs +++ b/compiler/typecheck/TcEvidence.hs @@ -18,11 +18,12 @@ module TcEvidence ( -- TcCoercion TcCoercion(..), LeftOrRight(..), pickLR, - mkTcReflCo, mkTcNomReflCo, + mkTcReflCo, mkTcNomReflCo, mkTcRepReflCo, mkTcTyConAppCo, mkTcAppCo, mkTcAppCos, mkTcFunCo, mkTcAxInstCo, mkTcUnbranchedAxInstCo, mkTcForAllCo, mkTcForAllCos, - mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcSubCo, - mkTcAxiomRuleCo, + mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcSubCo, maybeTcSubCo, + tcDowngradeRole, mkTcTransAppCo, + mkTcAxiomRuleCo, mkTcPhantomCo, tcCoercionKind, coVarsOfTcCo, isEqVar, mkTcCoVarCo, isTcReflCo, getTcCoVar_maybe, tcCoercionRole, eqVarRole @@ -30,12 +31,11 @@ module TcEvidence ( #include "HsVersions.h" import Var -import Coercion( LeftOrRight(..), pickLR, nthRole ) +import Coercion import PprCore () -- Instance OutputableBndr TyVar import TypeRep -- Knows type representation import TcType -import Type( tyConAppArgN, tyConAppTyCon_maybe, getEqPredTys, getEqPredRole, coAxNthLHS ) -import TysPrim( funTyCon ) +import Type import TyCon import CoAxiom import PrelNames @@ -91,6 +91,41 @@ differences * TcAxiomInstCo has a [TcCoercion] parameter, and not a [Type] parameter. This differs from the formalism, but corresponds to AxiomInstCo (see [Coercion axioms applied to coercions]). + +Note [mkTcTransAppCo] +~~~~~~~~~~~~~~~~~~~~~ +Suppose we have + + co1 :: a ~R Maybe + co2 :: b ~R Int + +and we want + + co3 :: a b ~R Maybe Int + +This seems sensible enough. But, we can't let (co3 = co1 co2), because +that's ill-roled! Note that mkTcAppCo requires a *nominal* second coercion. + +The way around this is to use transitivity: + + co3 = (co1 <b>_N) ; (Maybe co2) :: a b ~R Maybe Int + +Or, it's possible everything is the other way around: + + co1' :: Maybe ~R a + co2' :: Int ~R b + +and we want + + co3' :: Maybe Int ~R a b + +then + + co3' = (Maybe co2') ; (co1' <b>_N) + +This is exactly what `mkTcTransAppCo` builds for us. Information for all +the arguments tends to be to hand at call sites, so it's quicker than +using, say, tcCoercionKind. -} data TcCoercion @@ -112,6 +147,7 @@ data TcCoercion | TcSubCo TcCoercion | TcCastCo TcCoercion TcCoercion -- co1 |> co2 | TcLetCo TcEvBinds TcCoercion + | TcCoercion Coercion -- embed a Core Coercion deriving (Data.Data, Data.Typeable) isEqVar :: Var -> Bool @@ -159,29 +195,43 @@ mkTcSubCo :: TcCoercion -> TcCoercion mkTcSubCo co = ASSERT2( tcCoercionRole co == Nominal, ppr co) TcSubCo co -maybeTcSubCo2_maybe :: Role -- desired role - -> Role -- current role - -> TcCoercion -> Maybe TcCoercion -maybeTcSubCo2_maybe Representational Nominal = Just . mkTcSubCo -maybeTcSubCo2_maybe Nominal Representational = const Nothing -maybeTcSubCo2_maybe Phantom _ = panic "maybeTcSubCo2_maybe Phantom" -- not supported (not needed at the moment) -maybeTcSubCo2_maybe _ Phantom = const Nothing -maybeTcSubCo2_maybe _ _ = Just - -maybeTcSubCo2 :: Role -- desired role - -> Role -- current role - -> TcCoercion -> TcCoercion -maybeTcSubCo2 r1 r2 co - = case maybeTcSubCo2_maybe r1 r2 co of +-- See Note [Role twiddling functions] in Coercion +-- | Change the role of a 'TcCoercion'. Returns 'Nothing' if this isn't +-- a downgrade. +tcDowngradeRole_maybe :: Role -- desired role + -> Role -- current role + -> TcCoercion -> Maybe TcCoercion +tcDowngradeRole_maybe Representational Nominal = Just . mkTcSubCo +tcDowngradeRole_maybe Nominal Representational = const Nothing +tcDowngradeRole_maybe Phantom _ + = panic "tcDowngradeRole_maybe Phantom" + -- not supported (not needed at the moment) +tcDowngradeRole_maybe _ Phantom = const Nothing +tcDowngradeRole_maybe _ _ = Just + +-- See Note [Role twiddling functions] in Coercion +-- | Change the role of a 'TcCoercion'. Panics if this isn't a downgrade. +tcDowngradeRole :: Role -- ^ desired role + -> Role -- ^ current role + -> TcCoercion -> TcCoercion +tcDowngradeRole r1 r2 co + = case tcDowngradeRole_maybe r1 r2 co of Just co' -> co' - Nothing -> pprPanic "maybeTcSubCo2" (ppr r1 <+> ppr r2 <+> ppr co) + Nothing -> pprPanic "tcDowngradeRole" (ppr r1 <+> ppr r2 <+> ppr co) + +-- | If the EqRel is ReprEq, makes a TcSubCo; otherwise, does nothing. +-- Note that the input coercion should always be nominal. +maybeTcSubCo :: EqRel -> TcCoercion -> TcCoercion +maybeTcSubCo NomEq = id +maybeTcSubCo ReprEq = mkTcSubCo mkTcAxInstCo :: Role -> CoAxiom br -> Int -> [TcType] -> TcCoercion mkTcAxInstCo role ax index tys | ASSERT2( not (role == Nominal && ax_role == Representational) , ppr (ax, tys) ) - arity == n_tys = maybeTcSubCo2 role ax_role $ TcAxiomInstCo ax_br index rtys + arity == n_tys = tcDowngradeRole role ax_role $ + TcAxiomInstCo ax_br index rtys | otherwise = ASSERT( arity < n_tys ) - maybeTcSubCo2 role ax_role $ + tcDowngradeRole role ax_role $ foldl TcAppCo (TcAxiomInstCo ax_br index (take arity rtys)) (drop arity rtys) where @@ -202,9 +252,63 @@ mkTcUnbranchedAxInstCo role ax tys mkTcAppCo :: TcCoercion -> TcCoercion -> TcCoercion -- No need to deal with TyConApp on the left; see Note [TcCoercions] +-- Second coercion *must* be nominal mkTcAppCo (TcRefl r ty1) (TcRefl _ ty2) = TcRefl r (mkAppTy ty1 ty2) mkTcAppCo co1 co2 = TcAppCo co1 co2 +-- | Like `mkTcAppCo`, but allows the second coercion to be other than +-- nominal. See Note [mkTcTransAppCo]. Role r3 cannot be more stringent +-- than either r1 or r2. +mkTcTransAppCo :: Role -- ^ r1 + -> TcCoercion -- ^ co1 :: ty1a ~r1 ty1b + -> TcType -- ^ ty1a + -> TcType -- ^ ty1b + -> Role -- ^ r2 + -> TcCoercion -- ^ co2 :: ty2a ~r2 ty2b + -> TcType -- ^ ty2a + -> TcType -- ^ ty2b + -> Role -- ^ r3 + -> TcCoercion -- ^ :: ty1a ty2a ~r3 ty1b ty2b +mkTcTransAppCo r1 co1 ty1a ty1b r2 co2 ty2a ty2b r3 +-- How incredibly fiddly! Is there a better way?? + = case (r1, r2, r3) of + (_, _, Phantom) + -> mkTcPhantomCo (mkAppTy ty1a ty2a) (mkAppTy ty1b ty2b) + (_, _, Nominal) + -> ASSERT( r1 == Nominal && r2 == Nominal ) + mkTcAppCo co1 co2 + (Nominal, Nominal, Representational) + -> mkTcSubCo (mkTcAppCo co1 co2) + (_, Nominal, Representational) + -> ASSERT( r1 == Representational ) + mkTcAppCo co1 co2 + (Nominal, Representational, Representational) + -> go (mkTcSubCo co1) + (_ , _, Representational) + -> ASSERT( r1 == Representational && r2 == Representational ) + go co1 + where + go co1_repr + | Just (tc1b, tys1b) <- tcSplitTyConApp_maybe ty1b + , nextRole ty1b == r2 + = (co1_repr `mkTcAppCo` mkTcNomReflCo ty2a) `mkTcTransCo` + (mkTcTyConAppCo Representational tc1b + (zipWith mkTcReflCo (tyConRolesX Representational tc1b) tys1b + ++ [co2])) + + | Just (tc1a, tys1a) <- tcSplitTyConApp_maybe ty1a + , nextRole ty1a == r2 + = (mkTcTyConAppCo Representational tc1a + (zipWith mkTcReflCo (tyConRolesX Representational tc1a) tys1a + ++ [co2])) + `mkTcTransCo` + (co1_repr `mkTcAppCo` mkTcNomReflCo ty2b) + + | otherwise + = pprPanic "mkTcTransAppCo" (vcat [ ppr r1, ppr co1, ppr ty1a, ppr ty1b + , ppr r2, ppr co2, ppr ty2a, ppr ty2b + , ppr r3 ]) + mkTcSymCo :: TcCoercion -> TcCoercion mkTcSymCo co@(TcRefl {}) = co mkTcSymCo (TcSymCo co) = co @@ -223,6 +327,9 @@ mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion mkTcLRCo lr (TcRefl r ty) = TcRefl r (pickLR lr (tcSplitAppTy ty)) mkTcLRCo lr co = TcLRCo lr co +mkTcPhantomCo :: TcType -> TcType -> TcCoercion +mkTcPhantomCo = TcPhantomCo + mkTcAppCos :: TcCoercion -> [TcCoercion] -> TcCoercion mkTcAppCos co1 tys = foldl mkTcAppCo co1 tys @@ -272,6 +379,7 @@ tcCoercionKind co = go co case coaxrProves ax ts (map tcCoercionKind cs) of Just res -> res Nothing -> panic "tcCoercionKind: malformed TcAxiomRuleCo" + go (TcCoercion co) = coercionKind co eqVarRole :: EqVar -> Role eqVarRole cv = getEqPredRole (varType cv) @@ -303,6 +411,7 @@ tcCoercionRole = go go (TcAxiomRuleCo c _ _) = coaxrRole c go (TcCastCo c _) = go c go (TcLetCo _ c) = go c + go (TcCoercion co) = coercionRole co coVarsOfTcCo :: TcCoercion -> VarSet @@ -328,7 +437,10 @@ coVarsOfTcCo tc_co go (TcLetCo {}) = emptyVarSet -- Harumph. This does legitimately happen in the call -- to evVarsOfTerm in the DEBUG check of setEvBind go (TcAxiomRuleCo _ _ cos) = mapUnionVarSet go cos - + go (TcCoercion co) = -- the use of coVarsOfTcCo in dsTcCoercion will + -- fail if there are any proper, unlifted covars + ASSERT( isEmptyVarSet (coVarsOfCo co) ) + emptyVarSet -- We expect only coercion bindings, so use evTermCoercion go_bind :: EvBind -> VarSet @@ -377,6 +489,7 @@ ppr_co p (TcLRCo lr co) = pprPrefixApp p (ppr lr) [pprParendTcCo co] ppr_co p (TcSubCo co) = pprPrefixApp p (ptext (sLit "Sub")) [pprParendTcCo co] ppr_co p (TcAxiomRuleCo co ts ps) = maybeParen p TopPrec $ ppr_tc_axiom_rule_co co ts ps +ppr_co p (TcCoercion co) = pprPrefixApp p (text "Core co:") [ppr co] ppr_tc_axiom_rule_co :: CoAxiomRule -> [TcType] -> [TcCoercion] -> SDoc ppr_tc_axiom_rule_co co ts ps = ppr (coaxrName co) <> ppTs ts $$ nest 2 (ppPs ps) diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs index 99eb9150f8..34c2c4a04a 100644 --- a/compiler/typecheck/TcFlatten.hs +++ b/compiler/typecheck/TcFlatten.hs @@ -1,11 +1,12 @@ {-# LANGUAGE CPP #-} module TcFlatten( - FlattenEnv(..), FlattenMode(..), + FlattenEnv(..), FlattenMode(..), mkFlattenEnv, flatten, flattenMany, flatten_many, flattenFamApp, flattenTyVarOuter, unflatten, - eqCanRewrite, canRewriteOrSame + eqCanRewrite, eqCanRewriteFR, canRewriteOrSame, + CtFlavourRole, ctEvFlavourRole, ctFlavourRole ) where #include "HsVersions.h" @@ -17,6 +18,7 @@ import TcEvidence import TyCon import TypeRep import Kind( isSubKind ) +import Coercion ( tyConRolesX ) import Var import VarEnv import NameEnv @@ -26,9 +28,10 @@ import TcSMonad as TcS import DynFlags( DynFlags ) import Util +import MonadUtils ( zipWithAndUnzipM ) import Bag import FastString -import Control.Monad( when ) +import Control.Monad( when, liftM ) {- Note [The flattening story] @@ -562,12 +565,21 @@ so when the flattener encounters one, it first asks whether its transitive expansion contains any type function applications. If so, it expands the synonym and proceeds; if not, it simply returns the unexpanded synonym. + +Note [Flattener EqRels] +~~~~~~~~~~~~~~~~~~~~~~~ +When flattening, we need to know which equality relation -- nominal +or representation -- we should be respecting. The only difference is +that we rewrite variables by representational equalities when fe_eq_rel +is ReprEq. + -} data FlattenEnv - = FE { fe_mode :: FlattenMode - , fe_ev :: CtEvidence - } + = FE { fe_mode :: FlattenMode + , fe_loc :: CtLoc + , fe_flavour :: CtFlavour + , fe_eq_rel :: EqRel } -- See Note [Flattener EqRels] data FlattenMode -- Postcondition for all three: inert wrt the type substitution = FM_FlattenAll -- Postcondition: function-free @@ -581,6 +593,15 @@ data FlattenMode -- Postcondition for all three: inert wrt the type substitutio | FM_SubstOnly -- See Note [Flattening under a forall] +mkFlattenEnv :: FlattenMode -> CtEvidence -> FlattenEnv +mkFlattenEnv fm ctev = FE { fe_mode = fm + , fe_loc = ctEvLoc ctev + , fe_flavour = ctEvFlavour ctev + , fe_eq_rel = ctEvEqRel ctev } + +feRole :: FlattenEnv -> Role +feRole = eqRelRole . fe_eq_rel + {- Note [Lazy flattening] ~~~~~~~~~~~~~~~~~~~~~~ @@ -607,6 +628,21 @@ other examples where lazy flattening caused problems. Bottom line: FM_Avoid is unused for now (Nov 14). Note: T5321Fun got faster when I disabled FM_Avoid T5837 did too, but it's pathalogical anyway + +Note [Phantoms in the flattener] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have + +data Proxy p = Proxy + +and we're flattening (Proxy ty) w.r.t. ReprEq. Then, we know that `ty` +is really irrelevant -- it will be ignored when solving for representational +equality later on. So, we omit flattening `ty` entirely. This may +violate the expectation of "xi"s for a bit, but the canonicaliser will +soon throw out the phantoms when decomposing a TyConApp. (Or, the +canonicaliser will emit an insoluble, in which case the unflattened version +yields a better error message anyway.) + -} ------------------ @@ -614,35 +650,38 @@ flatten :: FlattenMode -> CtEvidence -> TcType -> TcS (Xi, TcCoercion) flatten mode ev ty = runFlatten (flatten_one fmode ty) where - fmode = FE { fe_mode = mode, fe_ev = ev } - -flattenMany :: FlattenMode -> CtEvidence -> [TcType] -> TcS ([Xi], [TcCoercion]) --- Flatten a bunch of types all at once. -flattenMany mode ev tys - = runFlatten (flatten_many fmode tys) + fmode = mkFlattenEnv mode ev + +flattenMany :: FlattenMode -> CtEvidence -> [Role] + -> [TcType] -> TcS ([Xi], [TcCoercion]) +-- Flatten a bunch of types all at once. Roles on the coercions returned +-- always match the corresponding roles passed in. +flattenMany mode ev roles tys + = runFlatten (flatten_many fmode roles tys) where - fmode = FE { fe_mode = mode, fe_ev = ev } + fmode = mkFlattenEnv mode ev -flattenFamApp :: FlattenMode -> CtEvidence -> TyCon -> [TcType] -> TcS (Xi, TcCoercion) +flattenFamApp :: FlattenMode -> CtEvidence + -> TyCon -> [TcType] -> TcS (Xi, TcCoercion) flattenFamApp mode ev tc tys = runFlatten (flatten_fam_app fmode tc tys) where - fmode = FE { fe_mode = mode, fe_ev = ev } + fmode = mkFlattenEnv mode ev ------------------ -flatten_many :: FlattenEnv -> [Type] -> TcS ([Xi], [TcCoercion]) --- Coercions :: Xi ~ Type +flatten_many :: FlattenEnv -> [Role] -> [Type] -> TcS ([Xi], [TcCoercion]) +-- Coercions :: Xi ~ Type, at roles given -- Returns True iff (no flattening happened) -- NB: The EvVar inside the 'fe_ev :: CtEvidence' is unused, -- we merely want (a) Given/Solved/Derived/Wanted info -- (b) the GivenLoc/WantedLoc for when we create new evidence -flatten_many fmode tys - = -- pprTrace "flattenMany" empty $ - go tys - where go [] = return ([],[]) - go (ty:tys) = do { (xi,co) <- flatten_one fmode ty - ; (xis,cos) <- go tys - ; return (xi:xis,co:cos) } +flatten_many fmode roles tys + = zipWithAndUnzipM go roles tys + where + go Nominal ty = flatten_one (fmode { fe_eq_rel = NomEq }) ty + go Representational ty = flatten_one (fmode { fe_eq_rel = ReprEq }) ty + go Phantom ty = -- See Note [Phantoms in the flattener] + return (ty, mkTcPhantomCo ty ty) ------------------ flatten_one :: FlattenEnv -> TcType -> TcS (Xi, TcCoercion) @@ -651,22 +690,38 @@ flatten_one :: FlattenEnv -> TcType -> TcS (Xi, TcCoercion) -- constraints. See Note [Flattening] for more detail. -- -- Postcondition: Coercion :: Xi ~ TcType +-- The role on the result coercion matches the EqRel in the FlattenEnv -flatten_one _ xi@(LitTy {}) = return (xi, mkTcNomReflCo xi) +flatten_one fmode xi@(LitTy {}) = return (xi, mkTcReflCo (feRole fmode) xi) flatten_one fmode (TyVarTy tv) = flattenTyVar fmode tv flatten_one fmode (AppTy ty1 ty2) = do { (xi1,co1) <- flatten_one fmode ty1 - ; (xi2,co2) <- flatten_one fmode ty2 - ; traceTcS "flatten/appty" (ppr ty1 $$ ppr ty2 $$ ppr xi1 $$ ppr co1 $$ ppr xi2 $$ ppr co2) - ; return (mkAppTy xi1 xi2, mkTcAppCo co1 co2) } + ; case (fe_eq_rel fmode, nextRole xi1) of + (NomEq, _) -> flatten_rhs xi1 co1 NomEq + (ReprEq, Nominal) -> flatten_rhs xi1 co1 NomEq + (ReprEq, Representational) -> flatten_rhs xi1 co1 ReprEq + (ReprEq, Phantom) -> + return (mkAppTy xi1 ty2, co1 `mkTcAppCo` mkTcNomReflCo ty2) } + where + flatten_rhs xi1 co1 eq_rel2 + = do { (xi2,co2) <- flatten_one (fmode { fe_eq_rel = eq_rel2 }) ty2 + ; traceTcS "flatten/appty" + (ppr ty1 $$ ppr ty2 $$ ppr xi1 $$ + ppr co1 $$ ppr xi2 $$ ppr co2) + ; let role1 = feRole fmode + role2 = eqRelRole eq_rel2 + ; return ( mkAppTy xi1 xi2 + , mkTcTransAppCo role1 co1 xi1 ty1 + role2 co2 xi2 ty2 + role1 ) } -- output should match fmode flatten_one fmode (FunTy ty1 ty2) = do { (xi1,co1) <- flatten_one fmode ty1 ; (xi2,co2) <- flatten_one fmode ty2 - ; return (mkFunTy xi1 xi2, mkTcFunCo Nominal co1 co2) } + ; return (mkFunTy xi1 xi2, mkTcFunCo (feRole fmode) co1 co2) } flatten_one fmode (TyConApp tc tys) @@ -709,8 +764,10 @@ flatten_one fmode ty@(ForAllTy {}) flattenTyConApp :: FlattenEnv -> TyCon -> [TcType] -> TcS (Xi, TcCoercion) flattenTyConApp fmode tc tys - = do { (xis, cos) <- flatten_many fmode tys - ; return (mkTyConApp tc xis, mkTcTyConAppCo Nominal tc cos) } + = do { (xis, cos) <- flatten_many fmode (tyConRolesX role tc) tys + ; return (mkTyConApp tc xis, mkTcTyConAppCo role tc cos) } + where + role = feRole fmode {- Note [Flattening synonyms] @@ -738,7 +795,7 @@ Under a forall, we (b) MUST NOT flatten type family applications Hence FMSubstOnly. -For (a) consider c ~ a, a ~ T (forall b. (b, [c]) +For (a) consider c ~ a, a ~ T (forall b. (b, [c])) If we don't apply the c~a substitution to the second constraint we won't see the occurs-check error. @@ -769,7 +826,9 @@ flatten_fam_app fmode tc tys -- Can be over-saturated do { let (tys1, tys_rest) = splitAt (tyConArity tc) tys ; (xi1, co1) <- flatten_exact_fam_app fmode tc tys1 -- co1 :: xi1 ~ F tys1 - ; (xis_rest, cos_rest) <- flatten_many fmode tys_rest + + -- all Nominal roles b/c the tycon is oversaturated + ; (xis_rest, cos_rest) <- flatten_many fmode (repeat Nominal) tys_rest -- cos_res :: xis_rest ~ tys_rest ; return ( mkAppTys xi1 xis_rest -- NB mkAppTys: rhs_xi might not be a type variable -- cf Trac #5655 @@ -780,33 +839,41 @@ flatten_exact_fam_app fmode tc tys = case fe_mode fmode of FM_FlattenAll -> flatten_exact_fam_app_fully fmode tc tys - FM_SubstOnly -> do { (xis, cos) <- flatten_many fmode tys + FM_SubstOnly -> do { (xis, cos) <- flatten_many fmode roles tys ; return ( mkTyConApp tc xis - , mkTcTyConAppCo Nominal tc cos ) } - - FM_Avoid tv flat_top -> do { (xis, cos) <- flatten_many fmode tys - ; if flat_top || tv `elemVarSet` tyVarsOfTypes xis - then flatten_exact_fam_app_fully fmode tc tys - else return ( mkTyConApp tc xis - , mkTcTyConAppCo Nominal tc cos ) } + , mkTcTyConAppCo (feRole fmode) tc cos ) } + + FM_Avoid tv flat_top -> + do { (xis, cos) <- flatten_many fmode roles tys + ; if flat_top || tv `elemVarSet` tyVarsOfTypes xis + then flatten_exact_fam_app_fully fmode tc tys + else return ( mkTyConApp tc xis + , mkTcTyConAppCo (feRole fmode) tc cos ) } + where + -- These are always going to be Nominal for now, + -- but not if #8177 is implemented + roles = tyConRolesX (feRole fmode) tc flatten_exact_fam_app_fully fmode tc tys - = do { (xis, cos) <- flatten_many (fmode { fe_mode = FM_FlattenAll })tys - ; let ret_co = mkTcTyConAppCo Nominal tc cos + = do { let roles = tyConRolesX (feRole fmode) tc + ; (xis, cos) <- flatten_many (fmode { fe_mode = FM_FlattenAll }) roles tys + ; let ret_co = mkTcTyConAppCo (feRole fmode) tc cos -- ret_co :: F xis ~ F tys - ctxt_ev = fe_ev fmode ; mb_ct <- lookupFlatCache tc xis ; case mb_ct of - Just (co, rhs_ty, ev) -- co :: F xis ~ fsk - | ev `canRewriteOrSame` ctxt_ev + Just (co, rhs_ty, flav) -- co :: F xis ~ fsk + | (flav, NomEq) `canRewriteOrSameFR` (feFlavourRole fmode) -> -- Usable hit in the flat-cache -- We certainly *can* use a Wanted for a Wanted do { traceTcS "flatten/flat-cache hit" $ (ppr tc <+> ppr xis $$ ppr rhs_ty $$ ppr co) ; (fsk_xi, fsk_co) <- flatten_one fmode rhs_ty -- The fsk may already have been unified, so flatten it -- fsk_co :: fsk_xi ~ fsk - ; return (fsk_xi, fsk_co `mkTcTransCo` mkTcSymCo co `mkTcTransCo` ret_co) } + ; return (fsk_xi, fsk_co `mkTcTransCo` + maybeTcSubCo (fe_eq_rel fmode) + (mkTcSymCo co) `mkTcTransCo` + ret_co) } -- :: fsk_xi ~ F xis -- Try to reduce the family application right now @@ -816,14 +883,17 @@ flatten_exact_fam_app_fully fmode tc tys Just (norm_co, norm_ty) -> do { (xi, final_co) <- flatten_one fmode norm_ty ; let co = norm_co `mkTcTransCo` mkTcSymCo final_co - ; extendFlatCache tc xis (co, xi, ctxt_ev) + ; extendFlatCache tc xis ( co, xi + , fe_flavour fmode ) ; return (xi, mkTcSymCo co `mkTcTransCo` ret_co) } ; Nothing -> do { let fam_ty = mkTyConApp tc xis - ; (ev, fsk) <- newFlattenSkolem ctxt_ev fam_ty + ; (ev, fsk) <- newFlattenSkolem (fe_flavour fmode) + (fe_loc fmode) + fam_ty ; let fsk_ty = mkTyVarTy fsk co = ctEvCoercion ev - ; extendFlatCache tc xis (co, fsk_ty, ev) + ; extendFlatCache tc xis (co, fsk_ty, ctEvFlavour ev) -- The new constraint (F xis ~ fsk) is not necessarily inert -- (e.g. the LHS may be a redex) so we must put it in the work list @@ -834,7 +904,9 @@ flatten_exact_fam_app_fully fmode tc tys ; emitFlatWork ct ; traceTcS "flatten/flat-cache miss" $ (ppr fam_ty $$ ppr fsk $$ ppr ev) - ; return (fsk_ty, mkTcSymCo co `mkTcTransCo` ret_co) } + ; return (fsk_ty, maybeTcSubCo (fe_eq_rel fmode) + (mkTcSymCo co) + `mkTcTransCo` ret_co) } } } } {- Note [Reduce type family applications eagerly] @@ -853,7 +925,6 @@ result. Doing so can save lots of work when the same redex shows up more than once. Note that we record the link from the redex all the way to its *final* value, not just the single step reduction. - ************************************************************************ * * Flattening a type variable @@ -890,7 +961,8 @@ Definition [Applying a generalised substitution] If S is a generalised substitution S(f,a) = t, if (a -fs-> t) in S, and fs >= f = a, otherwise -Application extends naturally to types S(f,t) +Application extends naturally to types S(f,t), modulo roles. +See Note [Flavours with roles]. Theorem: S(f,a) is well defined as a function. Proof: Suppose (a -f1-> t1) and (a -f2-> t2) are both in S, @@ -933,8 +1005,11 @@ guarantee that this recursive use will terminate. (K2a) not (fs >= fs) or (K2b) not (fw >= fs) or (K2c) a not in s - or (K3) if (b -fs-> a) is in S then not (fw >= fs) - (a stronger version of (K2)) + (K3) If (b -fs-> s) is in S with (fw >= fs), then + (K3a) If the role of fs is nominal: s /= a + (K3b) If the role of fs is representational: EITHER + a not in s, OR + the path from the top of s to a includes at least one non-newtype then the extended substition T = S+(a -fw-> t) is an inert generalised substitution. @@ -952,6 +1027,8 @@ The idea is that * Note that kicking out is a Bad Thing, because it means we have to re-process a constraint. The less we kick out, the better. + TODO: Make sure that kicking out really *is* a Bad Thing. We've assumed + this but haven't done the empirical study to check. * Assume we have G>=G, G>=W, D>=D, and that's all. Then, when performing a unification we add a new given a -G-> ty. But doing so does NOT require @@ -992,10 +1069,11 @@ Key lemma to make it watertight. Under the conditions of the Main Theorem, forall f st fw >= f, a is not in S^k(f,t), for any k +Also, consider roles more carefully. See Note [Flavours with roles]. Completeness ~~~~~~~~~~~~~ -K3: completeness. (K3) is not ncessary for the extended substitution +K3: completeness. (K3) is not necessary for the extended substitution to be inert. In fact K1 could be made stronger by saying ... then (not (fw >= fs) or not (fs >= fs)) But it's not enough for S to be inert; we also want completeness. @@ -1026,40 +1104,48 @@ in the same way as So if we kick out one, we should kick out the other. The orientation is somewhat accidental. ------------------------ -RAE: To prove that K3 is sufficient for completeness (as opposed to a rule that -looked for `a` *anywhere* on the RHS, not just at the top), we need this property: -All types in the inert set are "rigid". Here, rigid means that a type is one of -two things: a type that can equal only itself, or a type variable. Because the -inert set defines rewritings for type variables, a type variable can be considered -rigid because it will be rewritten only to a rigid type. - -In the current world, this rigidity property is true: all type families are -flattened away before adding equalities to the inert set. But, when we add -representational equality, that is no longer true! Newtypes are not rigid -w.r.t. representational equality. Accordingly, we would to change (K3) thus: - -(K3) If (b -fs-> s) is in S with (fw >= fs), then - (K3a) If the role of fs is nominal: s /= a - (K3b) If the role of fs is representational: EITHER - a not in s, OR - the path from the top of s to a includes at least one non-newtype - -SPJ/DV: this looks important... follow up - ------------------------ -RAE: Do we have evidence to support our belief that kicking out is bad? I can -imagine scenarios where kicking out *more* equalities is more efficient, in that -kicking out a Given, say, might then discover that the Given is reflexive and -thus can be dropped. Once this happens, then the Given is no longer used in -rewriting, making later flattenings faster. I tend to thing that, probably, -kicking out is something to avoid, but it would be nice to have data to support -this conclusion. And, that data is not terribly hard to produce: we can just -twiddle some settings and then time the testsuite in some sort of controlled -environment. - -SPJ: yes it would be good to do that. +When considering roles, we also need the second clause (K3b). Consider + + inert-item a -W/R-> b c + work-item c -G/N-> a + +The work-item doesn't get rewritten by the inert, because (>=) doesn't hold. +We've satisfied conditions (T1)-(T3) and (K1) and (K2). If all we had were +condition (K3a), then we would keep the inert around and add the work item. +But then, consider if we hit the following: + + work-item2 b -G/N-> Id +where + + newtype Id x = Id x + +For similar reasons, if we only had (K3a), we wouldn't kick the +representational inert out. And then, we'd miss solving the inert, which +now reduced to reflexivity. The solution here is to kick out representational +inerts whenever the tyvar of a work item is "exposed", where exposed means +not under some proper data-type constructor, like [] or Maybe. See +isTyVarExposed in TcType. This is encoded in (K3b). + +Note [Flavours with roles] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +The system described in Note [The inert equalities] discusses an abstract +set of flavours. In GHC, flavours have two components: the flavour proper, +taken from {Wanted, Derived, Given}; and the equality relation (often called +role), taken from {NomEq, ReprEq}. When substituting w.r.t. the inert set, +as described in Note [The inert equalities], we must be careful to respect +roles. For example, if we have + + inert set: a -G/R-> Int + b -G/R-> Bool + + type role T nominal representational + +and we wish to compute S(W/R, T a b), the correct answer is T a Bool, NOT +T Int Bool. The reason is that T's first parameter has a nominal role, and +thus rewriting a to Int in T a b is wrong. Indeed, this non-congruence of +subsitution means that the proof in Note [The inert equalities] may need +to be revisited, but we don't think that the end conclusion is wrong. -} flattenTyVar :: FlattenEnv -> TcTyVar -> TcS (Xi, TcCoercion) @@ -1071,11 +1157,11 @@ flattenTyVar :: FlattenEnv -> TcTyVar -> TcS (Xi, TcCoercion) -- -- Postcondition: co : xi ~ tv flattenTyVar fmode tv - = do { mb_yes <- flattenTyVarOuter (fe_ev fmode) tv + = do { mb_yes <- flattenTyVarOuter fmode tv ; case mb_yes of Left tv' -> -- Done do { traceTcS "flattenTyVar1" (ppr tv $$ ppr (tyVarKind tv')) - ; return (ty', mkTcNomReflCo ty') } + ; return (ty', mkTcReflCo (feRole fmode) ty') } where ty' = mkTyVarTy tv' @@ -1085,9 +1171,8 @@ flattenTyVar fmode tv ; return (ty2, co2 `mkTcTransCo` co1) } } -flattenTyVarOuter, flattenTyVarFinal - :: CtEvidence -> TcTyVar - -> TcS (Either TyVar (TcType, TcCoercion)) +flattenTyVarOuter :: FlattenEnv -> TcTyVar + -> TcS (Either TyVar (TcType, TcCoercion)) -- Look up the tyvar in -- a) the internal MetaTyVar box -- b) the tyvar binds @@ -1095,14 +1180,16 @@ flattenTyVarOuter, flattenTyVarFinal -- Return (Left tv') if it is not found, tv' has a properly zonked kind -- (Right (ty, co) if found, with co :: ty ~ tv; -flattenTyVarOuter ctxt_ev tv +flattenTyVarOuter fmode tv | not (isTcTyVar tv) -- Happens when flatten under a (forall a. ty) - = flattenTyVarFinal ctxt_ev tv -- So ty contains refernces to the non-TcTyVar a + = Left `liftM` flattenTyVarFinal fmode tv + -- So ty contains refernces to the non-TcTyVar a + | otherwise = do { mb_ty <- isFilledMetaTyVar_maybe tv ; case mb_ty of { Just ty -> do { traceTcS "Following filled tyvar" (ppr tv <+> equals <+> ppr ty) - ; return (Right (ty, mkTcNomReflCo ty)) } ; + ; return (Right (ty, mkTcReflCo (feRole fmode) ty)) } ; Nothing -> -- Try in the inert equalities @@ -1112,25 +1199,34 @@ flattenTyVarOuter ctxt_ev tv Just (ct:_) -- If the first doesn't work, -- the subsequent ones won't either | CTyEqCan { cc_ev = ctev, cc_tyvar = tv, cc_rhs = rhs_ty } <- ct - , eqCanRewrite ctev ctxt_ev + , ctEvFlavourRole ctev `eqCanRewriteFR` feFlavourRole fmode -> do { traceTcS "Following inert tyvar" (ppr tv <+> equals <+> ppr rhs_ty $$ ppr ctev) - ; return (Right (rhs_ty, mkTcSymCo (ctEvCoercion ctev))) } - -- NB: ct is Derived then (fe_ev fmode) must be also, hence + ; let rewrite_co1 = mkTcSymCo (ctEvCoercion ctev) + rewrite_co = case (ctEvEqRel ctev, fe_eq_rel fmode) of + (ReprEq, _rel) -> ASSERT( _rel == ReprEq ) + -- if this ASSERT fails, then + -- eqCanRewriteFR answered incorrectly + rewrite_co1 + (NomEq, NomEq) -> rewrite_co1 + (NomEq, ReprEq) -> mkTcSubCo rewrite_co1 + + ; return (Right (rhs_ty, rewrite_co)) } + -- NB: ct is Derived then fmode must be also, hence -- we are not going to touch the returned coercion -- so ctEvCoercion is fine. - _other -> flattenTyVarFinal ctxt_ev tv + _other -> Left `liftM` flattenTyVarFinal fmode tv } } } -flattenTyVarFinal ctxt_ev tv +flattenTyVarFinal :: FlattenEnv -> TcTyVar -> TcS TyVar +flattenTyVarFinal fmode tv = -- Done, but make sure the kind is zonked do { let kind = tyVarKind tv - kind_fmode = FE { fe_ev = ctxt_ev, fe_mode = FM_SubstOnly } + kind_fmode = fmode { fe_mode = FM_SubstOnly } ; (new_knd, _kind_co) <- flatten_one kind_fmode kind - ; return (Left (setVarType tv new_knd)) } + ; return (setVarType tv new_knd) } {- - Note [An alternative story for the inert substitution] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ (This entire note is just background, left here in case we ever want @@ -1201,19 +1297,39 @@ casee, so we don't care. -} eqCanRewrite :: CtEvidence -> CtEvidence -> Bool +eqCanRewrite ev1 ev2 = ctEvFlavourRole ev1 `eqCanRewriteFR` ctEvFlavourRole ev2 + +-- | Whether or not one 'Ct' can rewrite another is determined by its +-- flavour and its equality relation +type CtFlavourRole = (CtFlavour, EqRel) + +-- | Extract the flavour and role from a 'CtEvidence' +ctEvFlavourRole :: CtEvidence -> CtFlavourRole +ctEvFlavourRole ev = (ctEvFlavour ev, ctEvEqRel ev) + +-- | Extract the flavour and role from a 'Ct' +ctFlavourRole :: Ct -> CtFlavourRole +ctFlavourRole = ctEvFlavourRole . cc_ev + +-- | Extract the flavour and role from a 'FlattenEnv' +feFlavourRole :: FlattenEnv -> CtFlavourRole +feFlavourRole (FE { fe_flavour = flav, fe_eq_rel = eq_rel }) + = (flav, eq_rel) + +eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool -- Very important function! -- See Note [eqCanRewrite] -eqCanRewrite (CtGiven {}) _ = True -eqCanRewrite (CtDerived {}) (CtDerived {}) = True -- Derived can't solve wanted/given -eqCanRewrite _ _ = False +eqCanRewriteFR (Given, NomEq) (_, _) = True +eqCanRewriteFR (Given, ReprEq) (_, ReprEq) = True +eqCanRewriteFR _ _ = False canRewriteOrSame :: CtEvidence -> CtEvidence -> Bool -- See Note [canRewriteOrSame] -canRewriteOrSame (CtGiven {}) _ = True -canRewriteOrSame (CtWanted {}) (CtWanted {}) = True -canRewriteOrSame (CtWanted {}) (CtDerived {}) = True -canRewriteOrSame (CtDerived {}) (CtDerived {}) = True -canRewriteOrSame _ _ = False +canRewriteOrSame ev1 ev2 = ev1 `eqCanRewrite` ev2 || + ctEvFlavourRole ev1 == ctEvFlavourRole ev2 + +canRewriteOrSameFR :: CtFlavourRole -> CtFlavourRole -> Bool +canRewriteOrSameFR fr1 fr2 = fr1 `eqCanRewriteFR` fr2 || fr1 == fr2 {- Note [eqCanRewrite] @@ -1232,6 +1348,12 @@ Here we get [W] a ~ Bool but we do not want to complain about Bool ~ Char! +Accordingly, we also don't let Deriveds rewrite Deriveds. + +With the solver handling Coercible constraints like equality constraints, +the rewrite conditions must take role into account, never allowing +a representational equality to rewrite a nominal one. + Note [canRewriteOrSame] ~~~~~~~~~~~~~~~~~~~~~~~ canRewriteOrSame is similar but @@ -1319,13 +1441,16 @@ unflatten tv_eqs funeqs ---------------- finalise_eq :: Ct -> Cts -> TcS Cts - finalise_eq (CTyEqCan { cc_ev = ev, cc_tyvar = tv, cc_rhs = rhs }) rest + finalise_eq (CTyEqCan { cc_ev = ev, cc_tyvar = tv + , cc_rhs = rhs, cc_eq_rel = eq_rel }) rest | isFmvTyVar tv = do { ty1 <- zonkTcTyVar tv ; ty2 <- zonkTcType rhs ; let is_refl = ty1 `tcEqType` ty2 ; if is_refl then do { when (isWanted ev) $ - setEvBind (ctEvId ev) (EvCoercion $ mkTcNomReflCo rhs) + setEvBind (ctEvId ev) + (EvCoercion $ + mkTcReflCo (eqRelRole eq_rel) rhs) ; return rest } else return (mkNonCanonical ev `consCts` rest) } | otherwise @@ -1355,7 +1480,8 @@ tryFill dflags tv rhs ev ; case occurCheckExpand dflags tv rhs' of OC_OK rhs'' -- Normal case: fill the tyvar -> do { when (isWanted ev) $ - setEvBind (ctEvId ev) (EvCoercion (mkTcNomReflCo rhs'')) + setEvBind (ctEvId ev) + (EvCoercion (mkTcReflCo (ctEvRole ev) rhs'')) ; setWantedTyBind tv rhs'' ; return True } diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs index f14c490844..16d4bfcb67 100644 --- a/compiler/typecheck/TcHsSyn.hs +++ b/compiler/typecheck/TcHsSyn.hs @@ -38,6 +38,7 @@ import TypeRep -- We can see the representation of types import TcType import TcMType ( defaultKindVarToStar, zonkQuantifiedTyVar, writeMetaTyVar ) import TcEvidence +import Coercion import TysPrim import TysWiredIn import Type @@ -1283,6 +1284,7 @@ zonkEvBind env (EvBind var term) -- See Note [Optimise coercion zonking] -- This has a very big effect on some programs (eg Trac #5030) ; let ty' = idType var' + ; case getEqPredTys_maybe ty' of Just (r, ty1, ty2) | ty1 `eqType` ty2 -> return (EvBind var' (EvCoercion (mkTcReflCo r ty1))) @@ -1409,7 +1411,7 @@ zonkTcTypeToType env ty -- The two interesting cases! go (TyVarTy tv) = zonkTyVarOcc env tv - go (ForAllTy tv ty) = ASSERT( isImmutableTyVar tv ) do + go (ForAllTy tv ty) = ASSERT( isImmutableTyVar tv ) do { (env', tv') <- zonkTyBndrX env tv ; ty' <- zonkTcTypeToType env' ty ; return (ForAllTy tv' ty') } @@ -1417,6 +1419,32 @@ zonkTcTypeToType env ty zonkTcTypeToTypes :: ZonkEnv -> [TcType] -> TcM [Type] zonkTcTypeToTypes env tys = mapM (zonkTcTypeToType env) tys +zonkCoToCo :: ZonkEnv -> Coercion -> TcM Coercion +zonkCoToCo env co + = go co + where + go (Refl r ty) = mkReflCo r <$> zonkTcTypeToType env ty + go (TyConAppCo r tc args) = mkTyConAppCo r tc <$> mapM go args + go (AppCo co arg) = mkAppCo <$> go co <*> go arg + go (AxiomInstCo ax ind args) = AxiomInstCo ax ind <$> mapM go args + go (UnivCo r ty1 ty2) = mkUnivCo r <$> zonkTcTypeToType env ty1 + <*> zonkTcTypeToType env ty2 + go (SymCo co) = mkSymCo <$> go co + go (TransCo co1 co2) = mkTransCo <$> go co1 <*> go co2 + go (NthCo n co) = mkNthCo n <$> go co + go (LRCo lr co) = mkLRCo lr <$> go co + go (InstCo co arg) = mkInstCo <$> go co <*> zonkTcTypeToType env arg + go (SubCo co) = mkSubCo <$> go co + go (AxiomRuleCo ax ts cs) = AxiomRuleCo ax <$> mapM (zonkTcTypeToType env) ts + <*> mapM go cs + + -- The two interesting cases! + go (CoVarCo cv) = return (mkCoVarCo $ zonkIdOcc env cv) + go (ForAllCo tv co) = ASSERT( isImmutableTyVar tv ) + do { (env', tv') <- zonkTyBndrX env tv + ; co' <- zonkCoToCo env' co + ; return (mkForAllCo tv' co') } + zonkTvCollecting :: TcRef TyVarSet -> UnboundTyVarZonker -- This variant collects unbound type variables in a mutable variable -- Works on both types and kinds @@ -1479,3 +1507,5 @@ zonkTcCoToCo env co ; cs' <- mapM go cs ; return (TcAxiomRuleCo co ts' cs') } + go (TcCoercion co) = do { co' <- zonkCoToCo env co + ; return (TcCoercion co') } diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index 026ff6d830..475e4904c7 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -19,14 +19,9 @@ import CoAxiom(sfInteractTop, sfInteractInert) import Var import TcType import PrelNames (knownNatClassName, knownSymbolClassName, ipClassNameKey ) -import TysWiredIn ( coercibleClass ) import Id( idType ) import Class import TyCon -import DataCon -import Name -import RdrName ( GlobalRdrEnv, lookupGRE_Name, mkRdrQual, is_as, - is_decl, Provenance(Imported), gre_prov ) import FunDeps import FamInst import Inst( tyVarsOfCt ) @@ -684,7 +679,7 @@ interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc = do { let matching_funeqs = findFunEqsByTyCon funeqs tc ; let interact = sfInteractInert ops args (lookupFlattenTyVar eqs fsk) do_one (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk, cc_ev = iev }) - = mapM_ (unifyDerived (ctEvLoc iev)) + = mapM_ (unifyDerived (ctEvLoc iev) Nominal) (interact iargs (lookupFlattenTyVar eqs ifsk)) do_one ct = pprPanic "interactFunEq" (ppr ct) ; mapM_ do_one matching_funeqs @@ -702,11 +697,12 @@ interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc interactFunEq _ wi = pprPanic "interactFunEq" (ppr wi) lookupFlattenTyVar :: TyVarEnv EqualCtList -> TcTyVar -> TcType --- ^ Look up a flatten-tyvar in the inert TyVarEqs +-- ^ Look up a flatten-tyvar in the inert nominal TyVarEqs; +-- this is used only when dealing with a CFunEqCan lookupFlattenTyVar inert_eqs ftv = case lookupVarEnv inert_eqs ftv of - Just (CTyEqCan { cc_rhs = rhs } : _) -> rhs - _ -> mkTyVarTy ftv + Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq } : _) -> rhs + _ -> mkTyVarTy ftv reactFunEq :: CtEvidence -> TcTyVar -- From this :: F tys ~ fsk1 -> CtEvidence -> TcTyVar -- Solve this :: F tys ~ fsk2 @@ -817,9 +813,12 @@ test when solving pairwise CFunEqCan. interactTyVarEq :: InertCans -> Ct -> TcS (StopOrContinue Ct) -- CTyEqCans are always consumed, so always returns Stop -interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv, cc_rhs = rhs , cc_ev = ev }) +interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv + , cc_rhs = rhs + , cc_ev = ev + , cc_eq_rel = eq_rel }) | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i } - <- findTyEqs (inert_eqs inerts) tv + <- findTyEqs inerts tv , ev_i `canRewriteOrSame` ev , rhs_i `tcEqType` rhs ] = -- Inert: a ~ b @@ -830,7 +829,7 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv, cc_rhs = rhs , cc_ev | Just tv_rhs <- getTyVar_maybe rhs , (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i } - <- findTyEqs (inert_eqs inerts) tv_rhs + <- findTyEqs inerts tv_rhs , ev_i `canRewriteOrSame` ev , rhs_i `tcEqType` mkTyVarTy tv ] = -- Inert: a ~ b @@ -842,10 +841,12 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv, cc_rhs = rhs , cc_ev | otherwise = do { tclvl <- getTcLevel - ; if canSolveByUnification tclvl ev tv rhs + ; if canSolveByUnification tclvl ev eq_rel tv rhs then do { solveByUnification ev tv rhs - ; n_kicked <- kickOutRewritable givenFlavour tv - -- givenFlavour because the tv := xi is given + ; n_kicked <- kickOutRewritable Given NomEq tv + -- Given because the tv := xi is given + -- NomEq because only nom. equalities are solved + -- by unification ; return (Stop ev (ptext (sLit "Spontaneously solved") <+> ppr_kicked n_kicked)) } else do { traceTcS "Can't solve tyvar equality" @@ -855,7 +856,9 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv, cc_rhs = rhs , cc_ev <+> text "is" <+> ppr (metaTyVarTcLevel tv)) , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs) , text "TcLevel =" <+> ppr tclvl ]) - ; n_kicked <- kickOutRewritable ev tv + ; n_kicked <- kickOutRewritable (ctEvFlavour ev) + (ctEvEqRel ev) + tv ; updInertCans (\ ics -> addInertCan ics workItem) ; return (Stop ev (ptext (sLit "Kept as inert") <+> ppr_kicked n_kicked)) } } @@ -864,8 +867,12 @@ interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi) -- @trySpontaneousSolve wi@ solves equalities where one side is a -- touchable unification variable. -- Returns True <=> spontaneous solve happened -canSolveByUnification :: TcLevel -> CtEvidence -> TcTyVar -> Xi -> Bool -canSolveByUnification tclvl gw tv xi +canSolveByUnification :: TcLevel -> CtEvidence -> EqRel + -> TcTyVar -> Xi -> Bool +canSolveByUnification tclvl gw eq_rel tv xi + | ReprEq <- eq_rel -- we never solve representational equalities this way. + = False + | isGiven gw -- See Note [Touchables and givens] = False @@ -893,6 +900,7 @@ solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS () -- Solve with the identity coercion -- Precondition: kind(xi) is a sub-kind of kind(tv) -- Precondition: CtEvidence is Wanted or Derived +-- Precondition: CtEvidence is nominal -- See [New Wanted Superclass Work] to see why solveByUnification -- must work for Derived as well as Wanted -- Returns: workItem where @@ -923,30 +931,24 @@ solveByUnification wd tv xi setEvBind (ctEvId wd) (EvCoercion (mkTcNomReflCo xi')) } -givenFlavour :: CtEvidence --- Used just to pass to kickOutRewritable --- and to guide 'flatten' for givens -givenFlavour = CtGiven { ctev_pred = panic "givenFlavour:ev" - , ctev_evtm = panic "givenFlavour:tm" - , ctev_loc = panic "givenFlavour:loc" } - ppr_kicked :: Int -> SDoc ppr_kicked 0 = empty ppr_kicked n = parens (int n <+> ptext (sLit "kicked out")) -kickOutRewritable :: CtEvidence -- Flavour of the equality that is +kickOutRewritable :: CtFlavour -- Flavour of the equality that is -- being added to the inert set + -> EqRel -- of the new equality -> TcTyVar -- The new equality is tv ~ ty -> TcS Int -kickOutRewritable new_ev new_tv - | not (new_ev `eqCanRewrite` new_ev) - = return 0 -- If new_ev can't rewrite itself, it can't rewrite +kickOutRewritable new_flavour new_eq_rel new_tv + | not ((new_flavour, new_eq_rel) `eqCanRewriteFR` (new_flavour, new_eq_rel)) + = return 0 -- If new_flavour can't rewrite itself, it can't rewrite -- anything else, so no need to kick out anything -- This is a common case: wanteds can't rewrite wanteds | otherwise = do { ics <- getInertCans - ; let (kicked_out, ics') = kick_out new_ev new_tv ics + ; let (kicked_out, ics') = kick_out new_flavour new_eq_rel new_tv ics ; setInertCans ics' ; updWorkListTcS (appendWorkList kicked_out) @@ -958,23 +960,23 @@ kickOutRewritable new_ev new_tv , ppr kicked_out ]) ; return (workListSize kicked_out) } -kick_out :: CtEvidence -> TcTyVar -> InertCans -> (WorkList, InertCans) -kick_out new_ev new_tv (IC { inert_eqs = tv_eqs - , inert_dicts = dictmap - , inert_funeqs = funeqmap - , inert_irreds = irreds - , inert_insols = insols }) +kick_out :: CtFlavour -> EqRel -> TcTyVar -> InertCans -> (WorkList, InertCans) +kick_out new_flavour new_eq_rel new_tv (IC { inert_eqs = tv_eqs + , inert_dicts = dictmap + , inert_funeqs = funeqmap + , inert_irreds = irreds + , inert_insols = insols }) = (kicked_out, inert_cans_in) where -- NB: Notice that don't rewrite -- inert_solved_dicts, and inert_solved_funeqs -- optimistically. But when we lookup we have to -- take the substitution into account - inert_cans_in = IC { inert_eqs = tv_eqs_in - , inert_dicts = dicts_in - , inert_funeqs = feqs_in - , inert_irreds = irs_in - , inert_insols = insols_in } + inert_cans_in = IC { inert_eqs = tv_eqs_in + , inert_dicts = dicts_in + , inert_funeqs = feqs_in + , inert_irreds = irs_in + , inert_insols = insols_in } kicked_out = WL { wl_eqs = tv_eqs_out , wl_funeqs = feqs_out @@ -982,22 +984,26 @@ kick_out new_ev new_tv (IC { inert_eqs = tv_eqs `andCts` insols_out) , wl_implics = emptyBag } - (tv_eqs_out, tv_eqs_in) = foldVarEnv kick_out_eqs ([], emptyVarEnv) tv_eqs - (feqs_out, feqs_in) = partitionFunEqs kick_out_ct funeqmap - (dicts_out, dicts_in) = partitionDicts kick_out_ct dictmap - (irs_out, irs_in) = partitionBag kick_out_irred irreds - (insols_out, insols_in) = partitionBag kick_out_ct insols + (tv_eqs_out, tv_eqs_in) = foldVarEnv kick_out_eqs ([], emptyVarEnv) tv_eqs + (feqs_out, feqs_in) = partitionFunEqs kick_out_ct funeqmap + (dicts_out, dicts_in) = partitionDicts kick_out_ct dictmap + (irs_out, irs_in) = partitionBag kick_out_irred irreds + (insols_out, insols_in) = partitionBag kick_out_ct insols -- Kick out even insolubles; see Note [Kick out insolubles] + can_rewrite :: CtEvidence -> Bool + can_rewrite = ((new_flavour, new_eq_rel) `eqCanRewriteFR`) . ctEvFlavourRole + kick_out_ct :: Ct -> Bool kick_out_ct ct = kick_out_ctev (ctEvidence ct) - kick_out_ctev ev = eqCanRewrite new_ev ev + kick_out_ctev :: CtEvidence -> Bool + kick_out_ctev ev = can_rewrite ev && new_tv `elemVarSet` tyVarsOfType (ctEvPred ev) -- See Note [Kicking out inert constraints] kick_out_irred :: Ct -> Bool - kick_out_irred ct = eqCanRewrite new_ev (ctEvidence ct) + kick_out_irred ct = can_rewrite (cc_ev ct) && new_tv `elemVarSet` closeOverKinds (tyVarsOfCt ct) -- See Note [Kicking out Irreds] @@ -1008,16 +1014,31 @@ kick_out new_ev new_tv (IC { inert_eqs = tv_eqs [] -> acc_in (eq1:_) -> extendVarEnv acc_in (cc_tyvar eq1) eqs_in) where - (eqs_out, eqs_in) = partition kick_out_eq eqs + (eqs_in, eqs_out) = partition keep_eq eqs - -- kick_out_eq implements kick-out criteria (K1-3) - -- in the main theorem of Note [The inert equalities] in TcFlatten - kick_out_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty, cc_ev = ev }) - = eqCanRewrite new_ev ev - && (tv == new_tv - || (ev `eqCanRewrite` ev && new_tv `elemVarSet` tyVarsOfType rhs_ty) - || case getTyVar_maybe rhs_ty of { Just tv_r -> tv_r == new_tv; Nothing -> False }) - kick_out_eq ct = pprPanic "kick_out_eq" (ppr ct) + -- implements criteria K1-K3 in Note [The inert equalities] in TcFlatten + keep_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty, cc_ev = ev + , cc_eq_rel = eq_rel }) + | tv == new_tv + = not (can_rewrite ev) -- (K1) + + | otherwise + = check_k2 && check_k3 + where + check_k2 = not (ev `eqCanRewrite` ev) + || not (can_rewrite ev) + || not (new_tv `elemVarSet` tyVarsOfType rhs_ty) + + check_k3 + | can_rewrite ev + = case eq_rel of + NomEq -> not (rhs_ty `eqType` mkTyVarTy new_tv) + ReprEq -> isTyVarExposed new_tv rhs_ty + + | otherwise + = True + + keep_eq ct = pprPanic "keep_eq" (ppr ct) {- Note [Kicking out inert constraints] @@ -1451,7 +1472,8 @@ instFunDepEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc }) ; mapM_ (do_one subst) eqs } where do_one subst (FDEq { fd_ty_left = ty1, fd_ty_right = ty2 }) - = unifyDerived loc (Pair (Type.substTy subst ty1) (Type.substTy subst ty2)) + = unifyDerived loc Nominal $ + Pair (Type.substTy subst ty1) (Type.substTy subst ty2) {- ********************************************************************************* @@ -1606,7 +1628,7 @@ doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc = do { inert_eqs <- getInertEqs ; let eqns = sfInteractTop ops args (lookupFlattenTyVar inert_eqs fsk) - ; mapM_ (unifyDerived loc) eqns } + ; mapM_ (unifyDerived loc Nominal) eqns } | otherwise = return () @@ -1616,9 +1638,10 @@ shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion -> TyCon -> [TcType] -> TcS (StopOrContinue Ct) shortCutReduction old_ev fsk ax_co fam_tc tc_args | isGiven old_ev - = runFlatten $ - do { let fmode = FE { fe_mode = FM_FlattenAll, fe_ev = old_ev } - ; (xis, cos) <- flatten_many fmode tc_args + = ASSERT( ctEvEqRel old_ev == NomEq ) + runFlatten $ + do { let fmode = mkFlattenEnv FM_FlattenAll old_ev + ; (xis, cos) <- flatten_many fmode (repeat Nominal) tc_args -- ax_co :: F args ~ G tc_args -- cos :: xis ~ tc_args -- old_ev :: F args ~ fsk @@ -1636,9 +1659,10 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args | otherwise = ASSERT( not (isDerived old_ev) ) -- Caller ensures this + ASSERT( ctEvEqRel old_ev == NomEq ) runFlatten $ - do { let fmode = FE { fe_mode = FM_FlattenAll, fe_ev = old_ev } - ; (xis, cos) <- flatten_many fmode tc_args + do { let fmode = mkFlattenEnv FM_FlattenAll old_ev + ; (xis, cos) <- flatten_many fmode (repeat Nominal) tc_args -- ax_co :: F args ~ G tc_args -- cos :: xis ~ tc_args -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk @@ -1670,7 +1694,7 @@ dischargeFmv evar fmv co xi = ASSERT2( not (fmv `elemVarSet` tyVarsOfType xi), ppr evar $$ ppr fmv $$ ppr xi ) do { setWantedTyBind fmv xi ; setEvBind evar (EvCoercion co) - ; n_kicked <- kickOutRewritable givenFlavour fmv + ; n_kicked <- kickOutRewritable Given NomEq fmv ; traceTcS "dischargeFuv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) } {- @@ -1965,14 +1989,6 @@ matchClassInst _ clas [ ty ] _ = panicTcS (text "Unexpected evidence for" <+> ppr (className clas) $$ vcat (map (ppr . idType) (classMethods clas))) -matchClassInst _ clas [ _k, ty1, ty2 ] loc - | clas == coercibleClass - = do { traceTcS "matchClassInst for" $ - quotes (pprClassPred clas [ty1,ty2]) <+> text "at depth" <+> ppr (ctLocDepth loc) - ; ev <- getCoercibleInst loc ty1 ty2 - ; traceTcS "matchClassInst returned" $ ppr ev - ; return ev } - matchClassInst inerts clas tys loc = do { dflags <- getDynFlags ; tclvl <- getTcLevel @@ -2053,188 +2069,7 @@ matchClassInst inerts clas tys loc -- by the overlap check with the instance environment. matchable _tys ct = pprPanic "Expecting dictionary!" (ppr ct) --- See Note [Coercible Instances] --- Changes to this logic should likely be reflected in coercible_msg in TcErrors. -getCoercibleInst :: CtLoc -> TcType -> TcType -> TcS LookupInstResult -getCoercibleInst loc ty1 ty2 - = do { -- Get some global stuff in scope, for nice pattern-guard based code in `go` - rdr_env <- getGlobalRdrEnvTcS - ; famenv <- getFamInstEnvs - ; go famenv rdr_env } - where - go :: FamInstEnvs -> GlobalRdrEnv -> TcS LookupInstResult - go famenv rdr_env - -- Also see [Order of Coercible Instances] - - -- Coercible a a (see case 1 in [Coercible Instances]) - | ty1 `tcEqType` ty2 - = return $ GenInst [] - $ EvCoercion (TcRefl Representational ty1) - - -- Coercible (forall a. ty) (forall a. ty') (see case 2 in [Coercible Instances]) - | tcIsForAllTy ty1 - , tcIsForAllTy ty2 - , let (tvs1,body1) = tcSplitForAllTys ty1 - (tvs2,body2) = tcSplitForAllTys ty2 - , equalLength tvs1 tvs2 - = do { ev_term <- deferTcSForAllEq Representational loc (tvs1,body1) (tvs2,body2) - ; return $ GenInst [] ev_term } - - -- Coercible NT a (see case 3 in [Coercible Instances]) - | Just (rep_tc, conc_ty, nt_co) <- tcInstNewTyConTF_maybe famenv ty1 - , dataConsInScope rdr_env rep_tc -- Do not look at all tyConsOfTyCon - = do { markDataConsAsUsed rdr_env rep_tc - ; (new_goals, residual_co) <- requestCoercible loc conc_ty ty2 - ; let final_co = nt_co `mkTcTransCo` residual_co - -- nt_co :: ty1 ~R conc_ty - -- residual_co :: conc_ty ~R ty2 - ; return $ GenInst new_goals (EvCoercion final_co) } - - -- Coercible a NT (see case 3 in [Coercible Instances]) - | Just (rep_tc, conc_ty, nt_co) <- tcInstNewTyConTF_maybe famenv ty2 - , dataConsInScope rdr_env rep_tc -- Do not look at all tyConsOfTyCon - = do { markDataConsAsUsed rdr_env rep_tc - ; (new_goals, residual_co) <- requestCoercible loc ty1 conc_ty - ; let final_co = residual_co `mkTcTransCo` mkTcSymCo nt_co - ; return $ GenInst new_goals (EvCoercion final_co) } - - -- Coercible (D ty1 ty2) (D ty1' ty2') (see case 4 in [Coercible Instances]) - | Just (tc1,tyArgs1) <- splitTyConApp_maybe ty1 - , Just (tc2,tyArgs2) <- splitTyConApp_maybe ty2 - , tc1 == tc2 - , nominalArgsAgree tc1 tyArgs1 tyArgs2 - = do { -- We want evidence for all type arguments of role R - arg_stuff <- forM (zip3 (tyConRoles tc1) tyArgs1 tyArgs2) $ \ (r,ta1,ta2) -> - case r of - Representational -> requestCoercible loc ta1 ta2 - Phantom -> return ([], TcPhantomCo ta1 ta2) - Nominal -> return ([], mkTcNomReflCo ta1) - -- ta1 == ta2, due to nominalArgsAgree - ; let (new_goals_s, arg_cos) = unzip arg_stuff - final_co = mkTcTyConAppCo Representational tc1 arg_cos - ; return $ GenInst (concat new_goals_s) (EvCoercion final_co) } - - -- Cannot solve this one - | otherwise - = return NoInstance - -nominalArgsAgree :: TyCon -> [Type] -> [Type] -> Bool -nominalArgsAgree tc tys1 tys2 = all ok $ zip3 (tyConRoles tc) tys1 tys2 - where ok (r,t1,t2) = r /= Nominal || t1 `tcEqType` t2 - -dataConsInScope :: GlobalRdrEnv -> TyCon -> Bool -dataConsInScope rdr_env tc = not hidden_data_cons - where - data_con_names = map dataConName (tyConDataCons tc) - hidden_data_cons = not (isWiredInName (tyConName tc)) && - (isAbstractTyCon tc || any not_in_scope data_con_names) - not_in_scope dc = null (lookupGRE_Name rdr_env dc) - -markDataConsAsUsed :: GlobalRdrEnv -> TyCon -> TcS () -markDataConsAsUsed rdr_env tc = addUsedRdrNamesTcS - [ mkRdrQual (is_as (is_decl imp_spec)) occ - | dc <- tyConDataCons tc - , let dc_name = dataConName dc - occ = nameOccName dc_name - gres = lookupGRE_Name rdr_env dc_name - , not (null gres) - , Imported (imp_spec:_) <- [gre_prov (head gres)] ] - -requestCoercible :: CtLoc -> TcType -> TcType - -> TcS ( [CtEvidence] -- Fresh goals to solve - , TcCoercion ) -- Coercion witnessing (Coercible t1 t2) -requestCoercible loc ty1 ty2 - = ASSERT2( typeKind ty1 `tcEqKind` typeKind ty2, ppr ty1 <+> ppr ty2) - do { new_ev <- newWantedEvVarNC loc' (mkCoerciblePred ty1 ty2) - ; return ( [new_ev], ctEvCoercion new_ev) } - -- Evidence for a Coercible constraint is always a coercion t1 ~R t2 - where - loc' = bumpCtLocDepth CountConstraints loc - {- -Note [Coercible Instances] -~~~~~~~~~~~~~~~~~~~~~~~~~~ -The class Coercible is special: There are no regular instances, and the user -cannot even define them (it is listed as an `abstractClass` in TcValidity). -Instead, the type checker will create instances and their evidence out of thin -air, in getCoercibleInst. The following "instances" are present: - - 1. instance Coercible a a - for any type a at any kind k. - - 2. instance (forall a. Coercible t1 t2) => Coercible (forall a. t1) (forall a. t2) - (which would be illegal to write like that in the source code, but we have - it nevertheless). - - 3. instance Coercible r b => Coercible (NT t1 t2 ...) b - instance Coercible a r => Coercible a (NT t1 t2 ...) - for a newtype constructor NT (or data family instance that resolves to a - newtype) where - * r is the concrete type of NT, instantiated with the arguments t1 t2 ... - * the constructor of NT is in scope. - - The newtype TyCon can appear undersaturated, but only if it has - enough arguments to apply the newtype coercion (which is eta-reduced). Examples: - newtype NT a = NT (Either a Int) - Coercible (NT Int) (Either Int Int) -- ok - newtype NT2 a b = NT2 (b -> a) - newtype NT3 a b = NT3 (b -> a) - Coercible (NT2 Int) (NT3 Int) -- cannot be derived - - 4. instance (Coercible t1_r t1'_r, Coercible t2_r t2_r',...) => - Coercible (C t1_r t2_r ... t1_p t2_p ... t1_n t2_n ...) - (C t1_r' t2_r' ... t1_p' t2_p' ... t1_n t2_n ...) - for a type constructor C where - * the nominal type arguments are not changed, - * the phantom type arguments may change arbitrarily - * the representational type arguments are again Coercible - - The type constructor can be used undersaturated; then the Coercible - instance is at a higher kind. This does not cause problems. - - -The type checker generates evidence in the form of EvCoercion, but the -TcCoercion therein has role Representational, which are turned into Core -coercions by dsEvTerm in DsBinds. - -The evidence for the second case is created by deferTcSForAllEq, for the other -cases by getCoercibleInst. - -When the constraint cannot be solved, it is treated as any other unsolved -constraint, i.e. it can turn up in an inferred type signature, or reported to -the user as a regular "Cannot derive instance ..." error. In the latter case, -coercible_msg in TcErrors gives additional explanations of why GHC could not -find a Coercible instance, so it duplicates some of the logic from -getCoercibleInst (in negated form). - -Note [Order of Coercible Instances] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -At first glance, the order of the various coercible instances doesn't matter, as -incoherence is no issue here: We do not care how the evidence is constructed, -as long as it is. - -But because of role annotations, the order *can* matter: - - newtype T a = MkT [a] - type role T nominal - - type family F a - type instance F Int = Bool - -Here T's declared role is more restrictive than its inferred role -(representational) would be. If MkT is not in scope, so that the -newtype-unwrapping instance is not available, then this coercible -instance would fail: - Coercible (T Bool) (T (F Int) -But MkT was in scope, *and* if we used it before decomposing on T, -we'd unwrap the newtype (on both sides) to get - Coercible Bool (F Int) -which succeeds. - -So our current decision is to apply case 3 (newtype-unwrapping) first, -followed by decomposition (case 4). This is strictly more powerful -if the newtype constructor is in scope. See Trac #9117 for a discussion. - Note [Instance and Given overlap] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Assume that we have an inert set that looks as follows: diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs index b95e0c3ee0..159635fd9f 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -143,7 +143,7 @@ newDict cls tys predTypeOccName :: PredType -> OccName predTypeOccName ty = case classifyPredType ty of ClassPred cls _ -> mkDictOcc (getOccName cls) - EqPred _ _ -> mkVarOccFS (fsLit "cobox") + EqPred _ _ _ -> mkVarOccFS (fsLit "cobox") TuplePred _ -> mkVarOccFS (fsLit "tup") IrredPred _ -> mkVarOccFS (fsLit "irred") @@ -929,6 +929,10 @@ zonkTidyOrigin env (KindEqOrigin ty1 ty2 orig) ; (env2, ty2') <- zonkTidyTcType env1 ty2 ; (env3, orig') <- zonkTidyOrigin env2 orig ; return (env3, KindEqOrigin ty1' ty2' orig') } +zonkTidyOrigin env (CoercibleOrigin ty1 ty2) + = do { (env1, ty1') <- zonkTidyTcType env ty1 + ; (env2, ty2') <- zonkTidyTcType env1 ty2 + ; return (env2, CoercibleOrigin ty1' ty2') } zonkTidyOrigin env (FunDepOrigin1 p1 l1 p2 l2) = do { (env1, p1') <- zonkTidyTcType env p1 ; (env2, p2') <- zonkTidyTcType env1 p2 diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index 17d84cbfda..be7d44def0 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -50,9 +50,10 @@ module TcRnTypes( isCDictCan_Maybe, isCFunEqCan_maybe, isCIrredEvCan, isCNonCanonical, isWantedCt, isDerivedCt, isGivenCt, isHoleCt, isTypedHoleCt, isPartialTypeSigCt, - ctEvidence, ctLoc, ctPred, + ctEvidence, ctLoc, ctPred, ctFlavour, ctEqRel, mkNonCanonical, mkNonCanonicalCt, - ctEvPred, ctEvLoc, ctEvTerm, ctEvCoercion, ctEvId, ctEvCheckDepth, + ctEvPred, ctEvLoc, ctEvEqRel, + ctEvTerm, ctEvCoercion, ctEvId, ctEvCheckDepth, WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC, andWC, unionsWC, addFlats, addImplics, mkFlatWC, addInsols, @@ -73,11 +74,14 @@ module TcRnTypes( CtEvidence(..), mkGivenLoc, isWanted, isGiven, isDerived, + ctEvRole, -- Constraint solver plugins TcPlugin(..), TcPluginResult(..), TcPluginSolver, TcPluginM, runTcPluginM, unsafeTcPluginTcM, + CtFlavour(..), ctEvFlavour, + -- Pretty printing pprEvVarTheta, pprEvVars, pprEvVarWithType, @@ -95,6 +99,7 @@ import CoreSyn import HscTypes import TcEvidence import Type +import CoAxiom ( Role ) import Class ( Class ) import TyCon ( TyCon ) import ConLike ( ConLike(..) ) @@ -1026,7 +1031,7 @@ data Ct | CTyEqCan { -- tv ~ rhs -- Invariants: -- * See Note [Applying the inert substitution] in TcFlatten - -- * tv not in tvs(xi) (occurs check) + -- * tv not in tvs(rhs) (occurs check) -- * If tv is a TauTv, then rhs has no foralls -- (this avoids substituting a forall for the tyvar in other types) -- * typeKind ty `subKind` typeKind tv @@ -1035,12 +1040,16 @@ data Ct -- but it has no top-level function. -- E.g. a ~ [F b] is fine -- but a ~ F b is not + -- * If the equality is representational, rhs has no top-level newtype + -- See Note [No top-level newtypes on RHS of representational + -- equalities] in TcCanonical -- * If rhs is also a tv, then it is oriented to give best chance of -- unification happening; eg if rhs is touchable then lhs is too cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant] cc_tyvar :: TcTyVar, - cc_rhs :: TcType -- Not necessarily function-free (hence not Xi) + cc_rhs :: TcType, -- Not necessarily function-free (hence not Xi) -- See invariants above + cc_eq_rel :: EqRel } | CFunEqCan { -- F xis ~ fsk @@ -1169,6 +1178,14 @@ ctPred :: Ct -> PredType -- See Note [Ct/evidence invariant] ctPred ct = ctEvPred (cc_ev ct) +-- | Get the flavour of the given 'Ct' +ctFlavour :: Ct -> CtFlavour +ctFlavour = ctEvFlavour . ctEvidence + +-- | Get the equality relation for the given 'Ct' +ctEqRel :: Ct -> EqRel +ctEqRel = ctEvEqRel . ctEvidence + dropDerivedWC :: WantedConstraints -> WantedConstraints -- See Note [Dropping derived constraints] dropDerivedWC wc@(WC { wc_flat = flats }) @@ -1532,6 +1549,14 @@ ctEvPred = ctev_pred ctEvLoc :: CtEvidence -> CtLoc ctEvLoc = ctev_loc +-- | Get the equality relation relevant for a 'CtEvidence' +ctEvEqRel :: CtEvidence -> EqRel +ctEvEqRel = predTypeEqRel . ctEvPred + +-- | Get the role relevant for a 'CtEvidence' +ctEvRole :: CtEvidence -> Role +ctEvRole = eqRelRole . ctEvEqRel + ctEvTerm :: CtEvidence -> EvTerm ctEvTerm (CtGiven { ctev_evtm = tm }) = tm ctEvTerm (CtWanted { ctev_evar = ev }) = EvId ev @@ -1569,6 +1594,31 @@ isDerived (CtDerived {}) = True isDerived _ = False {- +%************************************************************************ +%* * + CtFlavour +%* * +%************************************************************************ + +Just an enum type that tracks whether a constraint is wanted, derived, +or given, when we need to separate that info from the constraint itself. + +-} + +data CtFlavour = Given | Wanted | Derived + deriving Eq + +instance Outputable CtFlavour where + ppr Given = text "[G]" + ppr Wanted = text "[W]" + ppr Derived = text "[D]" + +ctEvFlavour :: CtEvidence -> CtFlavour +ctEvFlavour (CtWanted {}) = Wanted +ctEvFlavour (CtGiven {}) = Given +ctEvFlavour (CtDerived {}) = Derived + +{- ************************************************************************ * * SubGoalDepth @@ -1864,6 +1914,7 @@ data CtOrigin | KindEqOrigin TcType TcType -- A kind equality arising from unifying these two types CtOrigin -- originally arising from this + | CoercibleOrigin TcType TcType -- a Coercible constraint | IPOccOrigin HsIPName -- Occurrence of an implicit parameter @@ -1945,8 +1996,13 @@ pprCtOrigin (DerivOriginDC dc n) pprCtOrigin (DerivOriginCoerce meth ty1 ty2) = hang (ctoHerald <+> ptext (sLit "the coercion of the method") <+> quotes (ppr meth)) - 2 (sep [ ptext (sLit "from type") <+> quotes (ppr ty1) - , ptext (sLit " to type") <+> quotes (ppr ty2) ]) + 2 (sep [ text "from type" <+> quotes (ppr ty1) + , nest 2 $ text "to type" <+> quotes (ppr ty2) ]) + +pprCtOrigin (CoercibleOrigin ty1 ty2) + = hang (ctoHerald <+> text "trying to show that the representations of") + 2 (quotes (ppr ty1) <+> text "and" $$ + quotes (ppr ty2) <+> text "are the same") pprCtOrigin simple_origin = ctoHerald <+> pprCtO simple_origin diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index 76200c5929..7c410b69a5 100644 --- a/compiler/typecheck/TcSMonad.hs +++ b/compiler/typecheck/TcSMonad.hs @@ -106,7 +106,6 @@ import Kind import TcType import DynFlags import Type -import CoAxiom(sfMatchFam) import TcEvidence import Class @@ -132,11 +131,11 @@ import UniqFM import Maybes ( orElse, firstJusts ) import TrieMap +import Control.Arrow ( first ) import Control.Monad( ap, when, unless, MonadPlus(..) ) import MonadUtils import Data.IORef import Data.List ( partition, foldl' ) -import Pair #ifdef DEBUG import Digraph @@ -258,11 +257,11 @@ extendWorkListCt :: Ct -> WorkList -> WorkList -- Agnostic extendWorkListCt ct wl = case classifyPredType (ctPred ct) of - EqPred ty1 _ + EqPred NomEq ty1 _ | Just (tc,_) <- tcSplitTyConApp_maybe ty1 , isTypeFamilyTyCon tc -> extendWorkListFunEq ct wl - | otherwise + EqPred {} -> extendWorkListEq ct wl _ -> extendWorkListNonEq ct wl @@ -387,7 +386,7 @@ Type-family equations, of form (ev : F tys ~ ty), live in three places -- See Note [Detailed InertCans Invariants] for more data InertCans = IC { inert_eqs :: TyVarEnv EqualCtList - -- All CTyEqCans; index is the LHS tyvar + -- All CTyEqCans with NomEq; index is the LHS tyvar , inert_funeqs :: FunEqMap Ct -- All CFunEqCans; index is the whole family head type. @@ -405,16 +404,18 @@ data InertCans } type EqualCtList = [Ct] --- EqualCtList invariants: --- * All are equalities --- * All these equalities have the same LHS --- * The list is never empty --- * No element of the list can rewrite any other --- --- From the fourth invariant it follows that the list is --- - A single Given, or --- - Multiple Wanteds, or --- - Multiple Deriveds +{- +Note [EqualCtList invariants] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + * All are equalities + * All these equalities have the same LHS + * The list is never empty + * No element of the list can rewrite any other + + From the fourth invariant it follows that the list is + - A single Given, or + - Any number of Wanteds and/or Deriveds +-} -- The Inert Set data InertSet @@ -422,13 +423,11 @@ data InertSet -- Canonical Given, Wanted, Derived (no Solved) -- Sometimes called "the inert set" - , inert_flat_cache :: FunEqMap (TcCoercion, TcType, CtEvidence) + , inert_flat_cache :: FunEqMap (TcCoercion, TcType, CtFlavour) -- See Note [Type family equations] -- If F tys :-> (co, ty, ev), -- then co :: F tys ~ ty -- - -- The 'ev' field is just for the G/W/D flavour, nothing more! - -- -- Just a hash-cons cache for use when flattening only -- These include entirely un-processed goals, so don't use -- them to solve a top-level goal, else you may end up solving @@ -439,7 +438,6 @@ data InertSet , inert_solved_dicts :: DictMap CtEvidence -- Of form ev :: C t1 .. tn -- Always the result of using a top-level instance declaration - -- See Note [Solved constraints] -- - Used to avoid creating a new EvVar when we have a new goal -- that we have solved in the past -- - Stored not necessarily as fully rewritten @@ -466,11 +464,11 @@ instance Outputable InertSet where emptyInert :: InertSet emptyInert - = IS { inert_cans = IC { inert_eqs = emptyVarEnv - , inert_dicts = emptyDicts - , inert_funeqs = emptyFunEqs - , inert_irreds = emptyCts - , inert_insols = emptyCts + = IS { inert_cans = IC { inert_eqs = emptyVarEnv + , inert_dicts = emptyDicts + , inert_funeqs = emptyFunEqs + , inert_irreds = emptyCts + , inert_insols = emptyCts } , inert_flat_cache = emptyFunEqs , inert_solved_dicts = emptyDictMap } @@ -479,9 +477,12 @@ emptyInert addInertCan :: InertCans -> Ct -> InertCans -- Precondition: item /is/ canonical addInertCan ics item@(CTyEqCan {}) - = ics { inert_eqs = extendVarEnv_C (\eqs _ -> item : eqs) - (inert_eqs ics) - (cc_tyvar item) [item] } + = ics { inert_eqs = add_eq (inert_eqs ics) item } + where + add_eq :: TyVarEnv EqualCtList -> Ct -> TyVarEnv EqualCtList + add_eq old_list it + = extendVarEnv_C (\old_eqs _new_eqs -> it : old_eqs) + old_list (cc_tyvar it) [it] addInertCan ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys }) = ics { inert_funeqs = insertFunEq (inert_funeqs ics) tc tys item } @@ -563,15 +564,15 @@ prepareInertsForImplications is@(IS { inert_cans = cans }) = is { inert_cans = getGivens cans , inert_flat_cache = emptyFunEqs } -- See Note [Do not inherit the flat cache] where - getGivens (IC { inert_eqs = eqs - , inert_irreds = irreds - , inert_funeqs = funeqs - , inert_dicts = dicts }) - = IC { inert_eqs = filterVarEnv is_given_ecl eqs - , inert_funeqs = filterFunEqs isGivenCt funeqs - , inert_irreds = Bag.filterBag isGivenCt irreds - , inert_dicts = filterDicts isGivenCt dicts - , inert_insols = emptyCts } + getGivens (IC { inert_eqs = eqs + , inert_irreds = irreds + , inert_funeqs = funeqs + , inert_dicts = dicts }) + = IC { inert_eqs = filterVarEnv is_given_ecl eqs + , inert_funeqs = filterFunEqs isGivenCt funeqs + , inert_irreds = Bag.filterBag isGivenCt irreds + , inert_dicts = filterDicts isGivenCt dicts + , inert_insols = emptyCts } is_given_ecl :: EqualCtList -> Bool is_given_ecl (ct:rest) | isGivenCt ct = ASSERT( null rest ) True @@ -611,8 +612,9 @@ them into Givens. There can *be* deriving CFunEqCans; see Trac #8129. -} getInertEqs :: TcS (TyVarEnv EqualCtList) -getInertEqs = do { inert <- getTcSInerts - ; return (inert_eqs (inert_cans inert)) } +getInertEqs + = do { inert <- getTcSInerts + ; return (inert_eqs (inert_cans inert)) } getUnsolvedInerts :: TcS ( Bag Implication , Cts -- Tyvar eqs: a ~ ty @@ -620,16 +622,19 @@ getUnsolvedInerts :: TcS ( Bag Implication , Cts -- Insoluble , Cts ) -- All others getUnsolvedInerts - = do { IC { inert_eqs = tv_eqs, inert_funeqs = fun_eqs + = do { IC { inert_eqs = tv_eqs + , inert_funeqs = fun_eqs , inert_irreds = irreds, inert_dicts = idicts , inert_insols = insols } <- getInertCans - ; let unsolved_tv_eqs = foldVarEnv (\cts rest -> foldr add_if_unsolved rest cts) + ; let unsolved_tv_eqs = foldVarEnv (\cts rest -> + foldr add_if_unsolved rest cts) emptyCts tv_eqs - unsolved_fun_eqs = foldFunEqs add_if_unsolved fun_eqs emptyCts - unsolved_irreds = Bag.filterBag is_unsolved irreds - unsolved_dicts = foldDicts add_if_unsolved idicts emptyCts - others = unsolved_irreds `unionBags` unsolved_dicts + unsolved_fun_eqs = foldFunEqs add_if_unsolved fun_eqs emptyCts + unsolved_irreds = Bag.filterBag is_unsolved irreds + unsolved_dicts = foldDicts add_if_unsolved idicts emptyCts + + others = unsolved_irreds `unionBags` unsolved_dicts ; implics <- getWorkListImplics @@ -724,6 +729,9 @@ are some wrinkles: * See Note [Let-bound skolems] for another wrinkle + * We do *not* need to worry about representational equalities, because + these do not affect the ability to float constraints. + Note [Let-bound skolems] ~~~~~~~~~~~~~~~~~~~~~~~~ If * the inert set contains a canonical Given CTyEqCan (a ~ ty) @@ -770,8 +778,8 @@ removeInertCt is ct = CFunEqCan { cc_fun = tf, cc_tyargs = tys } -> is { inert_funeqs = delFunEq (inert_funeqs is) tf tys } - CTyEqCan { cc_tyvar = x, cc_rhs = ty } -> - is { inert_eqs = delTyEq (inert_eqs is) x ty } + CTyEqCan { cc_tyvar = x, cc_rhs = ty } -> + is { inert_eqs = delTyEq (inert_eqs is) x ty } CIrredEvCan {} -> panic "removeInertCt: CIrredEvCan" CNonCanonical {} -> panic "removeInertCt: CNonCanonical" @@ -785,16 +793,19 @@ checkAllSolved = do { is <- getTcSInerts ; let icans = inert_cans is - unsolved_irreds = Bag.anyBag isWantedCt (inert_irreds icans) - unsolved_dicts = foldDicts ((||) . isWantedCt) (inert_dicts icans) False - unsolved_funeqs = foldFunEqs ((||) . isWantedCt) (inert_funeqs icans) False - unsolved_eqs = foldVarEnv ((||) . any isWantedCt) False (inert_eqs icans) + unsolved_irreds = Bag.anyBag isWantedCt (inert_irreds icans) + unsolved_dicts = foldDicts ((||) . isWantedCt) + (inert_dicts icans) False + unsolved_funeqs = foldFunEqs ((||) . isWantedCt) + (inert_funeqs icans) False + unsolved_eqs = foldVarEnv ((||) . any isWantedCt) False + (inert_eqs icans) ; return (not (unsolved_eqs || unsolved_irreds || unsolved_dicts || unsolved_funeqs || not (isEmptyBag (inert_insols icans)))) } -lookupFlatCache :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType, CtEvidence)) +lookupFlatCache :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType, CtFlavour)) lookupFlatCache fam_tc tys = do { IS { inert_flat_cache = flat_cache , inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts @@ -804,7 +815,7 @@ lookupFlatCache fam_tc tys lookup_inerts inert_funeqs | Just (CFunEqCan { cc_ev = ctev, cc_fsk = fsk }) <- findFunEqs inert_funeqs fam_tc tys - = Just (ctEvCoercion ctev, mkTyVarTy fsk, ctev) + = Just (ctEvCoercion ctev, mkTyVarTy fsk, ctEvFlavour ctev) | otherwise = Nothing lookup_flats flat_cache = findFunEq flat_cache fam_tc tys @@ -845,8 +856,8 @@ lookupSolvedDict (IS { inert_solved_dicts = solved }) loc cls tys type TyEqMap a = TyVarEnv a -findTyEqs :: TyEqMap EqualCtList -> TyVar -> EqualCtList -findTyEqs m tv = lookupVarEnv m tv `orElse` [] +findTyEqs :: InertCans -> TyVar -> EqualCtList +findTyEqs icans tv = lookupVarEnv (inert_eqs icans) tv `orElse` [] delTyEq :: TyEqMap EqualCtList -> TcTyVar -> TcType -> TyEqMap EqualCtList delTyEq m tv t = modifyVarEnv (filter (not . isThisOne)) m tv @@ -1510,10 +1521,10 @@ which will result in two Deriveds to end up in the insoluble set: -- Flatten skolems -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -newFlattenSkolem :: CtEvidence -> TcType -- F xis +newFlattenSkolem :: CtFlavour -> CtLoc + -> TcType -- F xis -> TcS (CtEvidence, TcTyVar) -- [W] x:: F xis ~ fsk -newFlattenSkolem ctxt_ev fam_ty - | isGiven ctxt_ev -- Make a given +newFlattenSkolem Given loc fam_ty = do { fsk <- wrapTcS $ do { uniq <- TcM.newUnique ; let name = TcM.mkTcTyVarName uniq (fsLit "fsk") @@ -1523,7 +1534,7 @@ newFlattenSkolem ctxt_ev fam_ty , ctev_loc = loc } ; return (ev, fsk) } - | otherwise -- Make a wanted +newFlattenSkolem _ loc fam_ty -- Make a wanted = do { fuv <- wrapTcS $ do { uniq <- TcM.newUnique ; ref <- TcM.newMutVar Flexi @@ -1534,10 +1545,8 @@ newFlattenSkolem ctxt_ev fam_ty ; return (mkTcTyVar name (typeKind fam_ty) details) } ; ev <- newWantedEvVarNC loc (mkTcEqPred fam_ty (mkTyVarTy fuv)) ; return (ev, fuv) } - where - loc = ctEvLoc ctxt_ev -extendFlatCache :: TyCon -> [Type] -> (TcCoercion, TcType, CtEvidence) -> TcS () +extendFlatCache :: TyCon -> [Type] -> (TcCoercion, TcType, CtFlavour) -> TcS () extendFlatCache tc xi_args stuff = do { dflags <- getDynFlags ; when (gopt Opt_FlatCache dflags) $ @@ -1651,8 +1660,8 @@ newGivenEvVars loc pts = mapM (newGivenEvVar loc) (filterOut (isKindEquality . f isKindEquality :: TcPredType -> Bool -- See Note [Do not create Given kind equalities] isKindEquality pred = case classifyPredType pred of - EqPred t1 _ -> isKind t1 - _ -> False + EqPred _ t1 _ -> isKind t1 + _ -> False {- Note [Do not create Given kind equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1732,33 +1741,9 @@ instDFunConstraints loc = mapM (newWantedEvVar loc) matchFam :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType)) -- Given (F tys) return (ty, co), where co :: F tys ~ ty matchFam tycon args - | isOpenTypeFamilyTyCon tycon = do { fam_envs <- getFamInstEnvs - ; let mb_match = tcLookupFamInst fam_envs tycon args - ; traceTcS "lookupFamInst" $ - vcat [ ppr tycon <+> ppr args - , pprTvBndrs (varSetElems (tyVarsOfTypes args)) - , ppr mb_match ] - ; case mb_match of - Nothing -> return Nothing - Just (FamInstMatch { fim_instance = famInst - , fim_tys = inst_tys }) - -> let co = mkTcUnbranchedAxInstCo Nominal (famInstAxiom famInst) inst_tys - ty = pSnd $ tcCoercionKind co - in return $ Just (co, ty) } - - | Just ax <- isClosedSynFamilyTyCon_maybe tycon - , Just (ind, inst_tys) <- chooseBranch ax args - = let co = mkTcAxInstCo Nominal ax ind inst_tys - ty = pSnd (tcCoercionKind co) - in return $ Just (co, ty) - - | Just ops <- isBuiltInSynFamTyCon_maybe tycon = - return $ do (r,ts,ty) <- sfMatchFam ops args - return (mkTcAxiomRuleCo r ts [], ty) - - | otherwise - = return Nothing + ; return $ fmap (first TcCoercion) $ + reduceTyFamApp_maybe fam_envs Nominal tycon args } {- Note [Residual implications] diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs index f9b891f993..ffe792ff79 100644 --- a/compiler/typecheck/TcSimplify.hs +++ b/compiler/typecheck/TcSimplify.hs @@ -20,7 +20,8 @@ import TcSMonad as TcS import TcInteract import Kind ( isKind, isSubKind, defaultKind_maybe ) import Inst -import Type ( classifyPredType, isIPClass, PredTree(..), getClassPredTys_maybe ) +import Type ( classifyPredType, isIPClass, PredTree(..) + , getClassPredTys_maybe, EqRel(..) ) import TyCon ( isTypeFamilyTyCon ) import Class ( Class ) import Id ( idType ) @@ -446,11 +447,13 @@ quantifyPred :: TyVarSet -- Quantifying over these quantifyPred qtvs pred = case classifyPredType pred of ClassPred cls tys - | isIPClass cls -> True -- See note [Inheriting implicit parameters] - | otherwise -> tyVarsOfTypes tys `intersectsVarSet` qtvs - EqPred ty1 ty2 -> quant_fun ty1 || quant_fun ty2 - IrredPred ty -> tyVarsOfType ty `intersectsVarSet` qtvs - TuplePred {} -> False + | isIPClass cls -> True -- See note [Inheriting implicit parameters] + | otherwise -> tyVarsOfTypes tys `intersectsVarSet` qtvs + EqPred NomEq ty1 ty2 -> quant_fun ty1 || quant_fun ty2 + -- representational equality is like a class constraint + EqPred ReprEq ty1 ty2 -> tyVarsOfTypes [ty1, ty2] `intersectsVarSet` qtvs + IrredPred ty -> tyVarsOfType ty `intersectsVarSet` qtvs + TuplePred {} -> False where -- Only quantify over (F tys ~ ty) if tys mentions a quantifed variable -- In particular, quanitifying over (F Int ~ ty) is a bit like quantifying @@ -648,7 +651,7 @@ simplifyRule name lhs_wanted rhs_wanted quantify_insol ct = not (isEqPred (ctPred ct)) quantify_normal ct - | EqPred t1 t2 <- classifyPredType (ctPred ct) + | EqPred NomEq t1 t2 <- classifyPredType (ctPred ct) = not (t1 `tcEqType` t2) | otherwise = True @@ -1253,7 +1256,7 @@ floatEqualities skols no_given_eqs wanteds@(WC { wc_flat = flats }) float_me :: Ct -> Bool float_me ct -- The constraint is un-flattened and de-cannonicalised | let pred = ctPred ct - , EqPred ty1 ty2 <- classifyPredType pred + , EqPred NomEq ty1 ty2 <- classifyPredType pred , tyVarsOfType pred `disjointVarSet` skol_set , useful_to_float ty1 ty2 = True diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index a00cd3b47a..2da1f9f15a 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -45,7 +45,7 @@ module TcType ( -------------------------------- -- Builders - mkPhiTy, mkSigmaTy, mkTcEqPred, + mkPhiTy, mkSigmaTy, mkTcEqPred, mkTcReprEqPred, mkTcEqPredRole, -------------------------------- -- Splitters @@ -56,7 +56,7 @@ module TcType ( tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs, tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, repSplitAppTy_maybe, tcInstHeadTyNotSynonym, tcInstHeadTyAppAllTyVars, - tcGetTyVar_maybe, tcGetTyVar, + tcGetTyVar_maybe, tcGetTyVar, nextRole, tcSplitSigmaTy, tcDeepSplitSigmaTy_maybe, --------------------------------- @@ -68,7 +68,7 @@ module TcType ( isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy, isIntegerTy, isBoolTy, isUnitTy, isCharTy, isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy, - isPredTy, isTyVarClassPred, + isPredTy, isTyVarClassPred, isTyVarExposed, --------------------------------- -- Misc type manipulators @@ -834,6 +834,19 @@ mkTcEqPred ty1 ty2 where k = typeKind ty1 +-- | Make a representational equality predicate +mkTcReprEqPred :: TcType -> TcType -> Type +mkTcReprEqPred ty1 ty2 + = mkTyConApp coercibleTyCon [k, ty1, ty2] + where + k = typeKind ty1 + +-- | Make an equality predicate at a given role. The role must not be Phantom. +mkTcEqPredRole :: Role -> TcType -> TcType -> Type +mkTcEqPredRole Nominal = mkTcEqPred +mkTcEqPredRole Representational = mkTcReprEqPred +mkTcEqPredRole Phantom = panic "mkTcEqPredRole Phantom" + -- @isTauTy@ tests for nested for-alls. It should not be called on a boxy type. isTauTy :: Type -> Bool @@ -1393,6 +1406,21 @@ is_tc uniq ty = case tcSplitTyConApp_maybe ty of Just (tc, _) -> uniq == getUnique tc Nothing -> False +-- | Does the given tyvar appear in the given type outside of any +-- non-newtypes? Assume we're looking for @a@. Says "yes" for +-- @a@, @N a@, @b a@, @a b@, @b (N a)@. Says "no" for +-- @[a]@, @Maybe a@, @T a@, where @N@ is a newtype and @T@ is a datatype. +isTyVarExposed :: TcTyVar -> TcType -> Bool +isTyVarExposed tv (TyVarTy tv') = tv == tv' +isTyVarExposed tv (TyConApp tc tys) + | isNewTyCon tc = any (isTyVarExposed tv) tys + | otherwise = False +isTyVarExposed _ (LitTy {}) = False +isTyVarExposed _ (FunTy {}) = False +isTyVarExposed tv (AppTy fun arg) = isTyVarExposed tv fun + || isTyVarExposed tv arg +isTyVarExposed _ (ForAllTy {}) = False + {- ************************************************************************ * * diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs index 0f3314723b..8575cf852f 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -495,10 +495,11 @@ check_pred_help under_syn dflags ctxt pred = check_pred_help True dflags ctxt pred' | otherwise = case classifyPredType pred of - ClassPred cls tys -> check_class_pred dflags ctxt pred cls tys - EqPred {} -> check_eq_pred dflags pred - TuplePred tys -> check_tuple_pred under_syn dflags ctxt pred tys - IrredPred _ -> check_irred_pred under_syn dflags ctxt pred + ClassPred cls tys -> check_class_pred dflags ctxt pred cls tys + EqPred NomEq _ _ -> check_eq_pred dflags pred + EqPred ReprEq ty1 ty2 -> check_repr_eq_pred dflags ctxt pred ty1 ty2 + TuplePred tys -> check_tuple_pred under_syn dflags ctxt pred tys + IrredPred _ -> check_irred_pred under_syn dflags ctxt pred check_class_pred :: DynFlags -> UserTypeCtxt -> PredType -> Class -> [TcType] -> TcM () check_class_pred dflags ctxt pred cls tys @@ -509,26 +510,31 @@ check_class_pred dflags ctxt pred cls tys (badIPPred pred) -- Check the form of the argument types - ; checkTc (check_class_pred_tys dflags ctxt tys) - (predTyVarErr (mkClassPred cls tys) $$ how_to_allow) + ; check_class_pred_tys dflags ctxt pred tys } where class_name = className cls arity = classArity cls n_tys = length tys arity_err = arityErr "Class" class_name arity n_tys - how_to_allow = parens (ptext (sLit "Use FlexibleContexts to permit this")) check_eq_pred :: DynFlags -> PredType -> TcM () check_eq_pred dflags pred - = -- Equational constraints are valid in all contexts if type - -- families are permitted + = -- Equational constraints are valid in all contexts if type + -- families are permitted checkTc (xopt Opt_TypeFamilies dflags || xopt Opt_GADTs dflags) (eqPredTyErr pred) +check_repr_eq_pred :: DynFlags -> UserTypeCtxt -> PredType + -> TcType -> TcType -> TcM () +check_repr_eq_pred dflags ctxt pred ty1 ty2 + = check_class_pred_tys dflags ctxt pred tys + where + tys = [ty1, ty2] + check_tuple_pred :: Bool -> DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM () check_tuple_pred under_syn dflags ctxt pred ts - = do { -- See Note [ConstraintKinds in predicates] + = do { -- See Note [ConstraintKinds in predicates] checkTc (under_syn || xopt Opt_ConstraintKinds dflags) (predTupleErr pred) ; mapM_ (check_pred_help under_syn dflags ctxt) ts } @@ -581,18 +587,23 @@ It is equally dangerous to allow them in instance heads because in that case the Paterson conditions may not detect duplication of a type variable or size change. -} ------------------------- -check_class_pred_tys :: DynFlags -> UserTypeCtxt -> [KindOrType] -> Bool -check_class_pred_tys dflags ctxt kts - = case ctxt of +check_class_pred_tys :: DynFlags -> UserTypeCtxt + -> PredType -> [KindOrType] -> TcM () +check_class_pred_tys dflags ctxt pred kts + = checkTc pred_ok (predTyVarErr pred $$ how_to_allow) + where + (_, tys) = span isKind kts -- see Note [Kind polymorphic type classes] + flexible_contexts = xopt Opt_FlexibleContexts dflags + undecidable_ok = xopt Opt_UndecidableInstances dflags + + pred_ok = case ctxt of SpecInstCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine InstDeclCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys -- Further checks on head and theta in -- checkInstTermination _ -> flexible_contexts || all tyvar_head tys - where - (_, tys) = span isKind kts -- see Note [Kind polymorphic type classes] - flexible_contexts = xopt Opt_FlexibleContexts dflags - undecidable_ok = xopt Opt_UndecidableInstances dflags + how_to_allow = parens (ptext (sLit "Use FlexibleContexts to permit this")) + ------------------------- tyvar_head :: Type -> Bool @@ -851,7 +862,7 @@ instTypeErr cls tys msg {- validDeivPred checks for OK 'deriving' context. See Note [Exotic -derived instance contexts] in TcSimplify. However the predicate is +derived instance contexts] in TcDeriv. However the predicate is here because it uses sizeTypes, fvTypes. Also check for a bizarre corner case, when the derived instance decl @@ -866,12 +877,16 @@ not converge. See Trac #5287. validDerivPred :: TyVarSet -> PredType -> Bool validDerivPred tv_set pred = case classifyPredType pred of - ClassPred _ tys -> hasNoDups fvs - && sizeTypes tys == length fvs - && all (`elemVarSet` tv_set) fvs - TuplePred ps -> all (validDerivPred tv_set) ps - _ -> True -- Non-class predicates are ok + ClassPred _ tys -> check_tys tys + -- EqPred ReprEq is a Coercible constraint; treat + -- like a class + EqPred ReprEq ty1 ty2 -> check_tys [ty1, ty2] + TuplePred ps -> all (validDerivPred tv_set) ps + _ -> True -- Non-class predicates are ok where + check_tys tys = hasNoDups fvs + && sizeTypes tys == length fvs + && all (`elemVarSet` tv_set) fvs fvs = fvType pred {- diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs index a16a146eab..71a003df3e 100644 --- a/compiler/types/Coercion.hs +++ b/compiler/types/Coercion.hs @@ -31,13 +31,16 @@ module Coercion ( -- ** Decomposition instNewTyCon_maybe, - topNormaliseNewType_maybe, + + NormaliseStepper, NormaliseStepResult(..), composeSteppers, + modifyStepResultCo, unwrapNewTypeStepper, + topNormaliseNewType_maybe, topNormaliseTypeX_maybe, decomposeCo, getCoVar_maybe, splitAppCo_maybe, splitForAllCo_maybe, nthRole, tyConRolesX, - nextRole, setNominalRole_maybe, + setNominalRole_maybe, -- ** Coercion variables mkCoVar, isCoVar, isCoVarType, coVarName, setCoVarName, setCoVarUnique, @@ -73,7 +76,7 @@ module Coercion ( tidyCo, tidyCos, -- * Other - applyCo + applyCo, ) where #include "HsVersions.h" @@ -98,7 +101,7 @@ import Unique import Pair import SrcLoc import PrelNames ( funTyConKey, eqPrimTyConKey, eqReprPrimTyConKey ) -import Control.Applicative +import Control.Applicative hiding ( empty ) #if __GLASGOW_HASKELL__ < 709 import Data.Traversable (traverse, sequenceA) #endif @@ -1159,15 +1162,7 @@ ltRole Representational _ = False ltRole Nominal Nominal = False ltRole Nominal _ = True --- if we wish to apply `co` to some other coercion, what would be its best --- role? -nextRole :: Coercion -> Role -nextRole (Refl r (TyConApp tc tys)) = head $ dropList tys (tyConRolesX r tc) -nextRole (TyConAppCo r tc cos) = head $ dropList cos (tyConRolesX r tc) -nextRole _ = Nominal - -- See note [Newtype coercions] in TyCon - -- | Create a coercion constructor (axiom) suitable for the given -- newtype 'TyCon'. The 'Name' should be that of a new coercion -- 'CoAxiom', the 'TyVar's the arguments expected by the @newtype@ and @@ -1225,16 +1220,94 @@ instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion) instNewTyCon_maybe tc tys | Just (tvs, ty, co_tc) <- unwrapNewTyConEtad_maybe tc -- Check for newtype , tvs `leLength` tys -- Check saturated enough - = Just (applyTysX tvs ty tys, mkUnbranchedAxInstCo Representational co_tc tys) + = Just ( applyTysX tvs ty tys + , mkUnbranchedAxInstCo Representational co_tc tys) | otherwise = Nothing +{- +************************************************************************ +* * + Type normalisation +* * +************************************************************************ +-} + +-- | A function to check if we can reduce a type by one step. Used +-- with 'topNormaliseTypeX_maybe'. +type NormaliseStepper = RecTcChecker + -> TyCon -- tc + -> [Type] -- tys + -> NormaliseStepResult + +-- | The result of stepping in a normalisation function. +-- See 'topNormaliseTypeX_maybe'. +data NormaliseStepResult + = NS_Done -- ^ nothing more to do + | NS_Abort -- ^ utter failure. The outer function should fail too. + | NS_Step RecTcChecker Type Coercion -- ^ we stepped, yielding new bits; + -- ^ co :: old type ~ new type + +modifyStepResultCo :: (Coercion -> Coercion) + -> NormaliseStepResult -> NormaliseStepResult +modifyStepResultCo f (NS_Step rec_nts ty co) = NS_Step rec_nts ty (f co) +modifyStepResultCo _ result = result + +-- | Try one stepper and then try the next, if the first doesn't make +-- progress. +composeSteppers :: NormaliseStepper -> NormaliseStepper + -> NormaliseStepper +composeSteppers step1 step2 rec_nts tc tys + = case step1 rec_nts tc tys of + success@(NS_Step {}) -> success + NS_Done -> step2 rec_nts tc tys + NS_Abort -> NS_Abort + +-- | A 'NormaliseStepper' that unwraps newtypes, careful not to fall into +-- a loop. If it would fall into a loop, it produces 'NS_Abort'. +unwrapNewTypeStepper :: NormaliseStepper +unwrapNewTypeStepper rec_nts tc tys + | Just (ty', co) <- instNewTyCon_maybe tc tys + = case checkRecTc rec_nts tc of + Just rec_nts' -> NS_Step rec_nts' ty' co + Nothing -> NS_Abort + + | otherwise + = NS_Done + +-- | A general function for normalising the top-level of a type. It continues +-- to use the provided 'NormaliseStepper' until that function fails, and then +-- this function returns. The roles of the coercions produced by the +-- 'NormaliseStepper' must all be the same, which is the role returned from +-- the call to 'topNormaliseTypeX_maybe'. +topNormaliseTypeX_maybe :: NormaliseStepper -> Type -> Maybe (Coercion, Type) +topNormaliseTypeX_maybe stepper + = go initRecTc Nothing + where + go rec_nts mb_co1 ty + | Just (tc, tys) <- splitTyConApp_maybe ty + = case stepper rec_nts tc tys of + NS_Step rec_nts' ty' co2 + -> go rec_nts' (mb_co1 `trans` co2) ty' + + NS_Done -> all_done + NS_Abort -> Nothing + + | otherwise + = all_done + where + all_done | Just co <- mb_co1 = Just (co, ty) + | otherwise = Nothing + + Nothing `trans` co2 = Just co2 + (Just co1) `trans` co2 = Just (co1 `mkTransCo` co2) + topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type) -- ^ Sometimes we want to look through a @newtype@ and get its associated coercion. -- This function strips off @newtype@ layers enough to reveal something that isn't --- a @newtype@. Specifically, here's the invariant: +-- a @newtype@, or responds False to ok_tc. Specifically, here's the invariant: -- --- > topNormaliseNewType_maybe rec_nts ty = Just (co, ty') +-- > topNormaliseNewType_maybe ty = Just (co, ty') -- -- then (a) @co : ty0 ~ ty'@. -- (b) ty' is not a newtype. @@ -1248,26 +1321,7 @@ topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type) -- topNormaliseNewType_maybe -- topNormaliseNewType_maybe ty - = go initRecTc Nothing ty - where - go rec_nts mb_co1 ty - | Just (tc, tys) <- splitTyConApp_maybe ty - , Just (ty', co2) <- instNewTyCon_maybe tc tys - , let co' = case mb_co1 of - Nothing -> co2 - Just co1 -> mkTransCo co1 co2 - = case checkRecTc rec_nts tc of - Just rec_nts' -> go rec_nts' (Just co') ty' - Nothing -> Nothing - -- Return Nothing overall if we get stuck - -- so that the return invariant is satisfied - -- See Note [Expanding newtypes] in TyCon - - | Just co1 <- mb_co1 -- Progress, but stopped on a non-newtype - = Just (co1, ty) - - | otherwise -- No progress - = Nothing + = topNormaliseTypeX_maybe unwrapNewTypeStepper ty {- ************************************************************************ @@ -1923,3 +1977,4 @@ Kind coercions are only of the form: Refl kind. They are only used to instantiate kind polymorphic type constructors in TyConAppCo. Remember that kind instantiation only happens with TyConApp, not AppTy. -} + diff --git a/compiler/types/FamInstEnv.hs b/compiler/types/FamInstEnv.hs index 2cfc0fc677..0b5bf2b521 100644 --- a/compiler/types/FamInstEnv.hs +++ b/compiler/types/FamInstEnv.hs @@ -2,7 +2,7 @@ -- -- FamInstEnv: Type checked family instance declarations -{-# LANGUAGE CPP, GADTs #-} +{-# LANGUAGE CPP, GADTs, ScopedTypeVariables #-} module FamInstEnv ( FamInst(..), FamFlavor(..), famInstAxiom, famInstTyCon, famInstRHS, @@ -20,11 +20,12 @@ module FamInstEnv ( FamInstMatch(..), lookupFamInstEnv, lookupFamInstEnvConflicts, - chooseBranch, isDominatedBy, + isDominatedBy, -- Normalisation topNormaliseType, topNormaliseType_maybe, normaliseType, normaliseTcApp, + reduceTyFamApp_maybe, -- Flattening flattenTys @@ -806,8 +807,10 @@ reduceTyFamApp_maybe envs role tc tys -- (e.g. the call in topNormaliseType_maybe) then we can -- unwrap data families as well as type-synonym families; -- otherwise only type-synonym families - , [FamInstMatch { fim_instance = fam_inst - , fim_tys = inst_tys }] <- lookupFamInstEnv envs tc ntys + , FamInstMatch { fim_instance = fam_inst + , fim_tys = inst_tys } : _ <- lookupFamInstEnv envs tc ntys + -- NB: Allow multiple matches because of compatible overlap + = let ax = famInstAxiom fam_inst co = mkUnbranchedAxInstCo role ax inst_tys ty = pSnd (coercionKind co) @@ -881,11 +884,9 @@ topNormaliseType env ty = case topNormaliseType_maybe env ty of Just (_co, ty') -> ty' Nothing -> ty -topNormaliseType_maybe :: FamInstEnvs - -> Type - -> Maybe (Coercion, Type) +topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Coercion, Type) --- Get rid of *outermost* (or toplevel) +-- ^ Get rid of *outermost* (or toplevel) -- * type function redex -- * newtypes -- using appropriate coercions. Specifically, if @@ -896,38 +897,20 @@ topNormaliseType_maybe :: FamInstEnvs -- -- However, ty' can be something like (Maybe (F ty)), where -- (F ty) is a redex. - +-- -- Its a bit like Type.repType, but handles type families too -- The coercion returned is always an R coercion topNormaliseType_maybe env ty - = go initRecTc Nothing ty + = topNormaliseTypeX_maybe stepper ty where - go :: RecTcChecker -> Maybe Coercion -> Type -> Maybe (Coercion, Type) - go rec_nts mb_co1 ty - = case splitTyConApp_maybe ty of - Just (tc, tys) -> go_tc tc tys - Nothing -> all_done mb_co1 - where - all_done Nothing = Nothing - all_done (Just co) = Just (co, ty) - - go_tc tc tys - | Just (ty', co2) <- instNewTyCon_maybe tc tys - = case checkRecTc rec_nts tc of - Just rec_nts' -> go rec_nts' (mb_co1 `trans` co2) ty' - Nothing -> Nothing -- No progress at all! - -- cf topNormaliseNewType_maybe - - | Just (co2, rhs) <- reduceTyFamApp_maybe env Representational tc tys - = go rec_nts (mb_co1 `trans` co2) rhs - - | otherwise - = all_done mb_co1 - - Nothing `trans` co2 = Just co2 - (Just co1) `trans` co2 = Just (co1 `mkTransCo` co2) - + stepper + = unwrapNewTypeStepper + `composeSteppers` + \ rec_nts tc tys -> + case reduceTyFamApp_maybe env Representational tc tys of + Just (co, rhs) -> NS_Step rec_nts rhs co + Nothing -> NS_Done --------------- normaliseTcApp :: FamInstEnvs -> Role -> TyCon -> [Type] -> (Coercion, Type) @@ -952,10 +935,10 @@ normaliseTcApp env role tc tys --------------- normaliseTcArgs :: FamInstEnvs -- environment with family instances - -> Role -- desired role of output coercion - -> TyCon -> [Type] -- tc tys - -> (Coercion, [Type]) -- (co, new_tys), where - -- co :: tc tys ~ tc new_tys + -> Role -- desired role of output coercion + -> TyCon -> [Type] -- tc tys + -> (Coercion, [Type]) -- (co, new_tys), where + -- co :: tc tys ~ tc new_tys normaliseTcArgs env role tc tys = (mkTyConAppCo role tc cois, ntys) where @@ -963,9 +946,9 @@ normaliseTcArgs env role tc tys --------------- normaliseType :: FamInstEnvs -- environment with family instances - -> Role -- desired role of output coercion - -> Type -- old type - -> (Coercion, Type) -- (coercion,new type), where + -> Role -- desired role of output coercion + -> Type -- old type + -> (Coercion, Type) -- (coercion,new type), where -- co :: old-type ~ new_type -- Normalise the input type, by eliminating *all* type-function redexes -- but *not* newtypes (which are visible to the programmer) @@ -974,7 +957,7 @@ normaliseType :: FamInstEnvs -- environment with family instances normaliseType env role (TyConApp tc tys) = normaliseTcApp env role tc tys -normaliseType _env role ty@(LitTy {}) = (Refl role ty, ty) +normaliseType _env role ty@(LitTy {}) = (mkReflCo role ty, ty) normaliseType env role (AppTy ty1 ty2) = let (coi1,nty1) = normaliseType env role ty1 (coi2,nty2) = normaliseType env Nominal ty2 @@ -987,7 +970,7 @@ normaliseType env role (ForAllTy tyvar ty1) = let (coi,nty1) = normaliseType env role ty1 in (mkForAllCo tyvar coi, ForAllTy tyvar nty1) normaliseType _ role ty@(TyVarTy _) - = (Refl role ty,ty) + = (mkReflCo role ty,ty) {- ************************************************************************ diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index 45422194e6..edc3067063 100644 --- a/compiler/types/Type.hs +++ b/compiler/types/Type.hs @@ -29,7 +29,7 @@ module Type ( mkTyConApp, mkTyConTy, tyConAppTyCon_maybe, tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs, - splitTyConApp_maybe, splitTyConApp, tyConAppArgN, + splitTyConApp_maybe, splitTyConApp, tyConAppArgN, nextRole, mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys, mkPiKinds, mkPiType, mkPiTypes, @@ -52,9 +52,10 @@ module Type ( isIPPred, isIPPred_maybe, isIPTyCon, isIPClass, -- Deconstructing predicate types - PredTree(..), classifyPredType, + PredTree(..), EqRel(..), eqRelRole, classifyPredType, getClassPredTys, getClassPredTys_maybe, getEqPredTys, getEqPredTys_maybe, getEqPredRole, + predTypeEqRel, -- ** Common type constructors funTyCon, @@ -169,6 +170,7 @@ import CoAxiom import Unique ( Unique, hasKey ) import BasicTypes ( Arity, RepArity ) import Util +import ListSetOps ( getNth ) import Outputable import FastString @@ -560,6 +562,20 @@ splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys) splitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res]) splitTyConApp_maybe _ = Nothing +-- | What is the role assigned to the next parameter of this type? Usually, +-- this will be 'Nominal', but if the type is a 'TyConApp', we may be able to +-- do better. The type does *not* have to be well-kinded when applied for this +-- to work! +nextRole :: Type -> Role +nextRole ty + | Just (tc, tys) <- splitTyConApp_maybe ty + , let num_tys = length tys + , num_tys < tyConArity tc + = tyConRoles tc `getNth` num_tys + + | otherwise + = Nominal + newTyConInstRhs :: TyCon -> [Type] -> Type -- ^ Unwrap one 'layer' of newtype on a type constructor and its -- arguments, using an eta-reduced version of the @newtype@ if possible. @@ -971,18 +987,36 @@ constraints build tuples. Decomposing PredType -} +-- | A choice of equality relation. This is separate from the type 'Role' +-- because 'Phantom' does not define a (non-trivial) equality relation. +data EqRel = NomEq | ReprEq + deriving (Eq, Ord) + +instance Outputable EqRel where + ppr NomEq = text "nominal equality" + ppr ReprEq = text "representational equality" + +eqRelRole :: EqRel -> Role +eqRelRole NomEq = Nominal +eqRelRole ReprEq = Representational + data PredTree = ClassPred Class [Type] - | EqPred Type Type + | EqPred EqRel Type Type | TuplePred [PredType] | IrredPred PredType classifyPredType :: PredType -> PredTree classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of - Just (tc, tys) | Just clas <- tyConClass_maybe tc - -> ClassPred clas tys + Just (tc, tys) | tc `hasKey` coercibleTyConKey + , let [_, ty1, ty2] = tys + -> EqPred ReprEq ty1 ty2 Just (tc, tys) | tc `hasKey` eqTyConKey , let [_, ty1, ty2] = tys - -> EqPred ty1 ty2 + -> EqPred NomEq ty1 ty2 + -- NB: Coercible is also a class, so this check must come *after* + -- the Coercible check + Just (tc, tys) | Just clas <- tyConClass_maybe tc + -> ClassPred clas tys Just (tc, tys) | isTupleTyCon tc -> TuplePred tys _ -> IrredPred ev_ty @@ -1001,7 +1035,8 @@ getEqPredTys :: PredType -> (Type, Type) getEqPredTys ty = case splitTyConApp_maybe ty of Just (tc, (_ : ty1 : ty2 : tys)) -> - ASSERT( null tys && (tc `hasKey` eqTyConKey || tc `hasKey` coercibleTyConKey) ) + ASSERT( null tys && (tc `hasKey` eqTyConKey + || tc `hasKey` coercibleTyConKey) ) (ty1, ty2) _ -> pprPanic "getEqPredTys" (ppr ty) @@ -1021,9 +1056,18 @@ getEqPredRole ty | tc `hasKey` coercibleTyConKey -> Representational _ -> pprPanic "getEqPredRole" (ppr ty) +-- | Get the equality relation relevant for a pred type. +predTypeEqRel :: PredType -> EqRel +predTypeEqRel ty + | Just (tc, _) <- splitTyConApp_maybe ty + , tc `hasKey` coercibleTyConKey + = ReprEq + | otherwise + = NomEq + {- -************************************************************************ -* * +%************************************************************************ +%* * Size * * ************************************************************************ diff --git a/compiler/utils/MonadUtils.hs b/compiler/utils/MonadUtils.hs index b066b404a1..edc863ab0c 100644 --- a/compiler/utils/MonadUtils.hs +++ b/compiler/utils/MonadUtils.hs @@ -11,7 +11,7 @@ module MonadUtils , liftIO1, liftIO2, liftIO3, liftIO4 - , zipWith3M + , zipWith3M, zipWith3M_, zipWithAndUnzipM , mapAndUnzipM, mapAndUnzip3M, mapAndUnzip4M , mapAccumLM , mapSndM @@ -71,6 +71,18 @@ zipWith3M f (x:xs) (y:ys) (z:zs) ; return $ r:rs } +zipWith3M_ :: Monad m => (a -> b -> c -> m d) -> [a] -> [b] -> [c] -> m () +zipWith3M_ f as bs cs = do { _ <- zipWith3M f as bs cs + ; return () } + +zipWithAndUnzipM :: Monad m + => (a -> b -> m (c, d)) -> [a] -> [b] -> m ([c], [d]) +zipWithAndUnzipM f (x:xs) (y:ys) + = do { (c, d) <- f x y + ; (cs, ds) <- zipWithAndUnzipM f xs ys + ; return (c:cs, d:ds) } +zipWithAndUnzipM _ _ _ = return ([], []) + -- | mapAndUnzipM for triples mapAndUnzip3M :: Monad m => (a -> m (b,c,d)) -> [a] -> m ([b],[c],[d]) mapAndUnzip3M _ [] = return ([],[],[]) diff --git a/compiler/utils/Util.hs b/compiler/utils/Util.hs index 7d44a5004b..aa3a19b64c 100644 --- a/compiler/utils/Util.hs +++ b/compiler/utils/Util.hs @@ -14,6 +14,8 @@ module Util ( zipEqual, zipWithEqual, zipWith3Equal, zipWith4Equal, zipLazy, stretchZipWith, zipWithAndUnzip, + filterByList, + unzipWith, mapFst, mapSnd, chkAppend, @@ -301,6 +303,15 @@ zipLazy :: [a] -> [b] -> [(a,b)] zipLazy [] _ = [] zipLazy (x:xs) ~(y:ys) = (x,y) : zipLazy xs ys +-- | 'filterByList' takes a list of Bools and a list of some elements and +-- filters out these elements for which the corresponding value in the list of +-- Bools is False. This function does not check whether the lists have equal +-- length. +filterByList :: [Bool] -> [a] -> [a] +filterByList (True:bs) (x:xs) = x : filterByList bs xs +filterByList (False:bs) (_:xs) = filterByList bs xs +filterByList _ _ = [] + stretchZipWith :: (a -> Bool) -> b -> (a->b->c) -> [a] -> [b] -> [c] -- ^ @stretchZipWith p z f xs ys@ stretches @ys@ by inserting @z@ in -- the places where @p@ returns @True@ diff --git a/testsuite/tests/deriving/should_fail/T1496.stderr b/testsuite/tests/deriving/should_fail/T1496.stderr index 867d6c6842..c9f3869846 100644 --- a/testsuite/tests/deriving/should_fail/T1496.stderr +++ b/testsuite/tests/deriving/should_fail/T1496.stderr @@ -1,11 +1,9 @@ T1496.hs:10:32: - Could not coerce from ‘c Int’ to ‘c Moo’ - because ‘c Int’ and ‘c Moo’ are different types. - arising from the coercion of the method ‘isInt’ from type - ‘forall (c :: * -> *). c Int -> c Int’ to type - ‘forall (c :: * -> *). c Int -> c Moo’ - Possible fix: - use a standalone 'deriving instance' declaration, - so you can specify the instance context yourself + Couldn't match representation of type ‘c Int’ with that of ‘c Moo’ + arising from the coercion of the method ‘isInt’ + from type ‘forall (c :: * -> *). c Int -> c Int’ + to type ‘forall (c :: * -> *). c Int -> c Moo’ + NB: We cannot know what roles the parameters to ‘c’ have; + we must assume that the role is nominal When deriving the instance for (IsInt Moo) diff --git a/testsuite/tests/deriving/should_fail/T4846.stderr b/testsuite/tests/deriving/should_fail/T4846.stderr index 8d6198ea8e..ab24af374e 100644 --- a/testsuite/tests/deriving/should_fail/T4846.stderr +++ b/testsuite/tests/deriving/should_fail/T4846.stderr @@ -1,9 +1,10 @@ T4846.hs:29:1: - Could not coerce from ‘Expr Bool’ to ‘Expr BOOL’ - because the first type argument of ‘Expr’ has role Nominal, - but the arguments ‘Bool’ and ‘BOOL’ differ - arising from a use of ‘GHC.Prim.coerce’ + Couldn't match type ‘BOOL’ with ‘Bool’ + arising from trying to show that the representations of + ‘Expr Bool’ and + ‘Expr BOOL’ are the same + Relevant role signatures: type role Expr nominal In the expression: GHC.Prim.coerce (mkExpr :: Expr Bool) :: Expr BOOL In an equation for ‘mkExpr’: diff --git a/testsuite/tests/deriving/should_fail/T5498.stderr b/testsuite/tests/deriving/should_fail/T5498.stderr index b613eae368..ac91aaa4d0 100644 --- a/testsuite/tests/deriving/should_fail/T5498.stderr +++ b/testsuite/tests/deriving/should_fail/T5498.stderr @@ -1,11 +1,11 @@ T5498.hs:30:39: - Could not coerce from ‘c a’ to ‘c (Down a)’ - because ‘c a’ and ‘c (Down a)’ are different types. - arising from the coercion of the method ‘intIso’ from type - ‘forall (c :: * -> *). c a -> c Int’ to type - ‘forall (c :: * -> *). c (Down a) -> c Int’ - Possible fix: - use a standalone 'deriving instance' declaration, - so you can specify the instance context yourself + Couldn't match representation of type ‘c a’ + with that of ‘c (Down a)’ + arising from the coercion of the method ‘intIso’ + from type ‘forall (c :: * -> *). c a -> c Int’ + to type ‘forall (c :: * -> *). c (Down a) -> c Int’ + Relevant role signatures: type role Down representational + NB: We cannot know what roles the parameters to ‘c’ have; + we must assume that the role is nominal When deriving the instance for (IntIso (Down a)) diff --git a/testsuite/tests/deriving/should_fail/T6147.stderr b/testsuite/tests/deriving/should_fail/T6147.stderr index a346ac3216..7f851a656b 100644 --- a/testsuite/tests/deriving/should_fail/T6147.stderr +++ b/testsuite/tests/deriving/should_fail/T6147.stderr @@ -1,11 +1,7 @@ T6147.hs:13:32: - Could not coerce from ‘T Int’ to ‘T Foo’ - because the first type argument of ‘T’ has role Nominal, - but the arguments ‘Int’ and ‘Foo’ differ - arising from the coercion of the method ‘foo’ from type - ‘Int -> T Int’ to type ‘Foo -> T Foo’ - Possible fix: - use a standalone 'deriving instance' declaration, - so you can specify the instance context yourself + Couldn't match type ‘Int’ with ‘Foo’ + arising from the coercion of the method ‘foo’ + from type ‘Int -> T Int’ to type ‘Foo -> T Foo’ + Relevant role signatures: type role T nominal When deriving the instance for (C Foo) diff --git a/testsuite/tests/deriving/should_fail/T7148.stderr b/testsuite/tests/deriving/should_fail/T7148.stderr index 9b1008a360..ba3a88b6fe 100644 --- a/testsuite/tests/deriving/should_fail/T7148.stderr +++ b/testsuite/tests/deriving/should_fail/T7148.stderr @@ -1,24 +1,20 @@ T7148.hs:27:40: - Could not coerce from ‘SameType b1 b’ to ‘SameType b1 (Tagged a b)’ - because the second type argument of ‘SameType’ has role Nominal, - but the arguments ‘b’ and ‘Tagged a b’ differ - arising from the coercion of the method ‘iso2’ from type - ‘forall b. SameType b () -> SameType b b’ to type - ‘forall b. SameType b () -> SameType b (Tagged a b)’ - Possible fix: - use a standalone 'deriving instance' declaration, - so you can specify the instance context yourself + Occurs check: cannot construct the infinite type: b ~ Tagged a b + arising from the coercion of the method ‘iso2’ + from type ‘forall b. SameType b () -> SameType b b’ + to type ‘forall b. SameType b () -> SameType b (Tagged a b)’ + Relevant role signatures: + type role Tagged phantom representational + type role SameType nominal nominal When deriving the instance for (IsoUnit (Tagged a b)) T7148.hs:27:40: - Could not coerce from ‘SameType b b1’ to ‘SameType (Tagged a b) b1’ - because the first type argument of ‘SameType’ has role Nominal, - but the arguments ‘b’ and ‘Tagged a b’ differ - arising from the coercion of the method ‘iso1’ from type - ‘forall b. SameType () b -> SameType b b’ to type - ‘forall b. SameType () b -> SameType (Tagged a b) b’ - Possible fix: - use a standalone 'deriving instance' declaration, - so you can specify the instance context yourself + Occurs check: cannot construct the infinite type: b ~ Tagged a b + arising from the coercion of the method ‘iso1’ + from type ‘forall b. SameType () b -> SameType b b’ + to type ‘forall b. SameType () b -> SameType (Tagged a b) b’ + Relevant role signatures: + type role Tagged phantom representational + type role SameType nominal nominal When deriving the instance for (IsoUnit (Tagged a b)) diff --git a/testsuite/tests/deriving/should_fail/T7148a.stderr b/testsuite/tests/deriving/should_fail/T7148a.stderr index 5f865d1f5c..4edb968702 100644 --- a/testsuite/tests/deriving/should_fail/T7148a.stderr +++ b/testsuite/tests/deriving/should_fail/T7148a.stderr @@ -1,11 +1,14 @@ T7148a.hs:19:50: - Could not coerce from ‘Result a b’ to ‘b’ - because ‘Result a b’ and ‘b’ are different types. - arising from the coercion of the method ‘coerce’ from type - ‘forall b. Proxy b -> a -> Result a b’ to type - ‘forall b. Proxy b -> IS_NO_LONGER a -> Result (IS_NO_LONGER a) b’ - Possible fix: - use a standalone 'deriving instance' declaration, - so you can specify the instance context yourself + Couldn't match representation of type ‘b’ with that of ‘Result a b’ + ‘b’ is a rigid type variable bound by + the type forall b1. Proxy b1 -> a -> Result a b1 at T7148a.hs:19:50 + arising from the coercion of the method ‘coerce’ + from type ‘forall b. Proxy b -> a -> Result a b’ + to type ‘forall b. + Proxy b -> IS_NO_LONGER a -> Result (IS_NO_LONGER a) b’ + Relevant role signatures: + type role IS_NO_LONGER representational + type role Result nominal nominal + type role Proxy phantom When deriving the instance for (Convert (IS_NO_LONGER a)) diff --git a/testsuite/tests/deriving/should_fail/T8851.stderr b/testsuite/tests/deriving/should_fail/T8851.stderr index 348f1f1714..0a2b384bd1 100644 --- a/testsuite/tests/deriving/should_fail/T8851.stderr +++ b/testsuite/tests/deriving/should_fail/T8851.stderr @@ -1,12 +1,16 @@ T8851.hs:24:12: - Could not coerce from ‘Monad Parser’ to ‘Monad MyParser’ - because the first type argument of ‘Monad’ has role Nominal, - but the arguments ‘Parser’ and ‘MyParser’ differ - arising from the coercion of the method ‘notFollowedBy’ from type - ‘forall a. (Monad Parser, Show a) => Parser a -> Parser ()’ to type - ‘forall a. (Monad MyParser, Show a) => MyParser a -> MyParser ()’ - Possible fix: - use a standalone 'deriving instance' declaration, - so you can specify the instance context yourself + Couldn't match type ‘Parser’ with ‘MyParser’ + arising from the coercion of the method ‘notFollowedBy’ + from type ‘forall a. + (Monad Parser, Show a) => + Parser a -> Parser ()’ + to type ‘forall a. + (Monad MyParser, Show a) => + MyParser a -> MyParser ()’ + Relevant role signatures: + type role Monad nominal + type role Show nominal + type role MyParser phantom + type role Parser phantom When deriving the instance for (Parsing MyParser) diff --git a/testsuite/tests/deriving/should_fail/T8984.hs b/testsuite/tests/deriving/should_fail/T8984.hs new file mode 100644 index 0000000000..6b0b39518d --- /dev/null +++ b/testsuite/tests/deriving/should_fail/T8984.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE ConstraintKinds, GeneralizedNewtypeDeriving #-} +module T8984 where + +class C a where + app :: a (a Int) + +newtype N cat a b = MkN (cat a b) deriving( C ) +-- The newtype coercion is N cat ~R cat diff --git a/testsuite/tests/deriving/should_fail/T8984.stderr b/testsuite/tests/deriving/should_fail/T8984.stderr new file mode 100644 index 0000000000..6606d66f63 --- /dev/null +++ b/testsuite/tests/deriving/should_fail/T8984.stderr @@ -0,0 +1,11 @@ + +T8984.hs:7:46: + Couldn't match representation of type ‘cat a (N cat a Int)’ + with that of ‘cat a (cat a Int)’ + arising from the coercion of the method ‘app’ + from type ‘cat a (cat a Int)’ to type ‘N cat a (N cat a Int)’ + Relevant role signatures: + type role N representational nominal nominal + NB: We cannot know what roles the parameters to ‘cat a’ have; + we must assume that the role is nominal + When deriving the instance for (C (N cat a)) diff --git a/testsuite/tests/deriving/should_fail/all.T b/testsuite/tests/deriving/should_fail/all.T index 54a6f95afc..df7957d9b0 100644 --- a/testsuite/tests/deriving/should_fail/all.T +++ b/testsuite/tests/deriving/should_fail/all.T @@ -53,3 +53,4 @@ test('T9071', normal, multimod_compile_fail, ['T9071','']) test('T9071_2', normal, compile_fail, ['']) test('T9687', normal, compile_fail, ['']) +test('T8984', normal, compile_fail, ['']) diff --git a/testsuite/tests/gadt/CasePrune.stderr b/testsuite/tests/gadt/CasePrune.stderr index db22c46a7d..1202d1b04e 100644 --- a/testsuite/tests/gadt/CasePrune.stderr +++ b/testsuite/tests/gadt/CasePrune.stderr @@ -1,11 +1,7 @@ CasePrune.hs:14:31: - Could not coerce from ‘T Int’ to ‘T A’ - because the first type argument of ‘T’ has role Nominal, - but the arguments ‘Int’ and ‘A’ differ - arising from the coercion of the method ‘ic’ from type ‘T Int’ - to type ‘T A’ - Possible fix: - use a standalone 'deriving instance' declaration, - so you can specify the instance context yourself + Couldn't match type ‘Int’ with ‘A’ + arising from the coercion of the method ‘ic’ + from type ‘T Int’ to type ‘T A’ + Relevant role signatures: type role T nominal When deriving the instance for (C A) diff --git a/testsuite/tests/ghci/scripts/GhciKinds.hs b/testsuite/tests/ghci/scripts/GhciKinds.hs index 4945814ff9..8e1af372ee 100644 --- a/testsuite/tests/ghci/scripts/GhciKinds.hs +++ b/testsuite/tests/ghci/scripts/GhciKinds.hs @@ -4,3 +4,7 @@ module GhciKinds where type family F a :: * type instance F [a] = a -> F a type instance F Int = Bool + +-- test ":kind!" in the presence of compatible overlap +type instance F (Maybe a) = Char +type instance F (Maybe Int) = Char diff --git a/testsuite/tests/ghci/scripts/GhciKinds.script b/testsuite/tests/ghci/scripts/GhciKinds.script index 310c2a8c3d..fa9401524c 100644 --- a/testsuite/tests/ghci/scripts/GhciKinds.script +++ b/testsuite/tests/ghci/scripts/GhciKinds.script @@ -3,3 +3,8 @@ :l GhciKinds :kind F [[[Int]]] :kind! F [[[Int]]] +:kind! F (Maybe Int) +:kind! F (Maybe Bool) + +:seti -XRankNTypes +:kind! forall a. F (Maybe a) diff --git a/testsuite/tests/ghci/scripts/GhciKinds.stdout b/testsuite/tests/ghci/scripts/GhciKinds.stdout index 3961994e09..e34b84a42a 100644 --- a/testsuite/tests/ghci/scripts/GhciKinds.stdout +++ b/testsuite/tests/ghci/scripts/GhciKinds.stdout @@ -3,3 +3,9 @@ Maybe :: * -> * F [[[Int]]] :: * F [[[Int]]] :: * = [[Int]] -> [Int] -> Int -> Bool +F (Maybe Int) :: * += Char +F (Maybe Bool) :: * += Char +forall a. F (Maybe a) :: * += Char diff --git a/testsuite/tests/ghci/scripts/ghci051.stderr b/testsuite/tests/ghci/scripts/ghci051.stderr index 327188f42a..3b6ad44d93 100644 --- a/testsuite/tests/ghci/scripts/ghci051.stderr +++ b/testsuite/tests/ghci/scripts/ghci051.stderr @@ -1,7 +1,7 @@ <interactive>:7:9: Couldn't match type ‘T’ - with ‘Ghci1.T’ + with ‘Ghci1.T’ NB: ‘T’ is defined at <interactive>:6:1-16 ‘Ghci1.T’ is defined at <interactive>:3:1-14 Expected type: T' diff --git a/testsuite/tests/indexed-types/should_fail/T9580.stderr b/testsuite/tests/indexed-types/should_fail/T9580.stderr index 19ceefb0ff..fdb457ae31 100644 --- a/testsuite/tests/indexed-types/should_fail/T9580.stderr +++ b/testsuite/tests/indexed-types/should_fail/T9580.stderr @@ -2,9 +2,10 @@ [2 of 2] Compiling T9580 ( T9580.hs, T9580.o ) T9580.hs:7:9: - Could not coerce from ‘Dimensional Int Double’ to ‘Double’ - because the data constructor ‘T9580a.Quantity'’ + Couldn't match representation of type ‘Double’ + with that of ‘Dimensional Int Double’ + Relevant role signatures: type role Dimensional nominal nominal + The data constructor ‘T9580a.Quantity'’ of newtype ‘Dimensional Int v’ is not in scope - arising from a use of ‘coerce’ In the expression: coerce x In an equation for ‘foo’: foo x = coerce x diff --git a/testsuite/tests/roles/should_fail/Roles10.stderr b/testsuite/tests/roles/should_fail/Roles10.stderr index 2102298269..4275385081 100644 --- a/testsuite/tests/roles/should_fail/Roles10.stderr +++ b/testsuite/tests/roles/should_fail/Roles10.stderr @@ -1,10 +1,7 @@ Roles10.hs:16:12: - Could not coerce from ‘Bool’ to ‘Char’ - because ‘Bool’ and ‘Char’ are different types. - arising from the coercion of the method ‘meth’ from type - ‘Int -> F Int’ to type ‘Age -> F Age’ - Possible fix: - use a standalone 'deriving instance' declaration, - so you can specify the instance context yourself + Couldn't match representation of type ‘Char’ with that of ‘Bool’ + arising from the coercion of the method ‘meth’ + from type ‘Int -> F Int’ to type ‘Age -> F Age’ + Relevant role signatures: type role F nominal When deriving the instance for (C Age) diff --git a/testsuite/tests/roles/should_fail/RolesIArray.stderr b/testsuite/tests/roles/should_fail/RolesIArray.stderr index aad2f2b18a..fa9e8fe57f 100644 --- a/testsuite/tests/roles/should_fail/RolesIArray.stderr +++ b/testsuite/tests/roles/should_fail/RolesIArray.stderr @@ -1,100 +1,93 @@ RolesIArray.hs:10:13: - Could not coerce from ‘UArray i Word64’ to ‘UArray i N’ - because the second type argument of ‘UArray’ has role Nominal, - but the arguments ‘Word64’ and ‘N’ differ - arising from the coercion of the method ‘Data.Array.Base.unsafeAccumArray’ - from type ‘forall e' i. - Ix i => - (Word64 -> e' -> Word64) - -> Word64 -> (i, i) -> [(Int, e')] -> UArray i Word64’ - to type ‘forall e' i. - Ix i => - (N -> e' -> N) -> N -> (i, i) -> [(Int, e')] -> UArray i N’ - Possible fix: - use a standalone 'deriving instance' declaration, - so you can specify the instance context yourself + Couldn't match type ‘Word64’ with ‘N’ + arising from the coercion of the method ‘Data.Array.Base.unsafeAccumArray’ + from type ‘forall e' i. + Ix i => + (Word64 -> e' -> Word64) + -> Word64 -> (i, i) -> [(Int, e')] -> UArray i Word64’ + to type ‘forall e' i. + Ix i => + (N -> e' -> N) -> N -> (i, i) -> [(Int, e')] -> UArray i N’ + Relevant role signatures: + type role Ix nominal + type role [] representational + type role (,) representational representational + type role UArray nominal nominal When deriving the instance for (IArray UArray N) RolesIArray.hs:10:13: - Could not coerce from ‘UArray i Word64’ to ‘UArray i N’ - because the second type argument of ‘UArray’ has role Nominal, - but the arguments ‘Word64’ and ‘N’ differ - arising from the coercion of the method ‘Data.Array.Base.unsafeAccum’ - from type ‘forall e' i. - Ix i => - (Word64 -> e' -> Word64) - -> UArray i Word64 -> [(Int, e')] -> UArray i Word64’ - to type ‘forall e' i. - Ix i => - (N -> e' -> N) -> UArray i N -> [(Int, e')] -> UArray i N’ - Possible fix: - use a standalone 'deriving instance' declaration, - so you can specify the instance context yourself + Couldn't match type ‘Word64’ with ‘N’ + arising from the coercion of the method ‘Data.Array.Base.unsafeAccum’ + from type ‘forall e' i. + Ix i => + (Word64 -> e' -> Word64) + -> UArray i Word64 -> [(Int, e')] -> UArray i Word64’ + to type ‘forall e' i. + Ix i => + (N -> e' -> N) -> UArray i N -> [(Int, e')] -> UArray i N’ + Relevant role signatures: + type role Ix nominal + type role [] representational + type role (,) representational representational + type role UArray nominal nominal When deriving the instance for (IArray UArray N) RolesIArray.hs:10:13: - Could not coerce from ‘UArray i Word64’ to ‘UArray i N’ - because the second type argument of ‘UArray’ has role Nominal, - but the arguments ‘Word64’ and ‘N’ differ - arising from the coercion of the method ‘Data.Array.Base.unsafeReplace’ - from type ‘forall i. - Ix i => - UArray i Word64 -> [(Int, Word64)] -> UArray i Word64’ - to type ‘forall i. - Ix i => - UArray i N -> [(Int, N)] -> UArray i N’ - Possible fix: - use a standalone 'deriving instance' declaration, - so you can specify the instance context yourself + Couldn't match type ‘Word64’ with ‘N’ + arising from the coercion of the method ‘Data.Array.Base.unsafeReplace’ + from type ‘forall i. + Ix i => + UArray i Word64 -> [(Int, Word64)] -> UArray i Word64’ + to type ‘forall i. Ix i => UArray i N -> [(Int, N)] -> UArray i N’ + Relevant role signatures: + type role Ix nominal + type role [] representational + type role (,) representational representational + type role UArray nominal nominal When deriving the instance for (IArray UArray N) RolesIArray.hs:10:13: - Could not coerce from ‘UArray i Word64’ to ‘UArray i N’ - because the second type argument of ‘UArray’ has role Nominal, - but the arguments ‘Word64’ and ‘N’ differ - arising from the coercion of the method ‘Data.Array.Base.unsafeAt’ - from type ‘forall i. Ix i => UArray i Word64 -> Int -> Word64’ - to type ‘forall i. Ix i => UArray i N -> Int -> N’ - Possible fix: - use a standalone 'deriving instance' declaration, - so you can specify the instance context yourself + Couldn't match type ‘Word64’ with ‘N’ + arising from the coercion of the method ‘Data.Array.Base.unsafeAt’ + from type ‘forall i. Ix i => UArray i Word64 -> Int -> Word64’ + to type ‘forall i. Ix i => UArray i N -> Int -> N’ + Relevant role signatures: + type role Ix nominal + type role UArray nominal nominal When deriving the instance for (IArray UArray N) RolesIArray.hs:10:13: - Could not coerce from ‘UArray i Word64’ to ‘UArray i N’ - because the second type argument of ‘UArray’ has role Nominal, - but the arguments ‘Word64’ and ‘N’ differ - arising from the coercion of the method ‘Data.Array.Base.unsafeArray’ - from type ‘forall i. - Ix i => - (i, i) -> [(Int, Word64)] -> UArray i Word64’ - to type ‘forall i. Ix i => (i, i) -> [(Int, N)] -> UArray i N’ - Possible fix: - use a standalone 'deriving instance' declaration, - so you can specify the instance context yourself + Couldn't match type ‘Word64’ with ‘N’ + arising from the coercion of the method ‘Data.Array.Base.unsafeArray’ + from type ‘forall i. + Ix i => + (i, i) -> [(Int, Word64)] -> UArray i Word64’ + to type ‘forall i. Ix i => (i, i) -> [(Int, N)] -> UArray i N’ + Relevant role signatures: + type role Ix nominal + type role [] representational + type role (,) representational representational + type role UArray nominal nominal When deriving the instance for (IArray UArray N) RolesIArray.hs:10:13: - Could not coerce from ‘UArray i Word64’ to ‘UArray i N’ - because the second type argument of ‘UArray’ has role Nominal, - but the arguments ‘Word64’ and ‘N’ differ - arising from the coercion of the method ‘Data.Array.Base.numElements’ - from type ‘forall i. Ix i => UArray i Word64 -> Int’ - to type ‘forall i. Ix i => UArray i N -> Int’ - Possible fix: - use a standalone 'deriving instance' declaration, - so you can specify the instance context yourself + Couldn't match type ‘Word64’ with ‘N’ + arising from the coercion of the method ‘Data.Array.Base.numElements’ + from type ‘forall i. Ix i => UArray i Word64 -> Int’ + to type ‘forall i. Ix i => UArray i N -> Int’ + Relevant role signatures: + type role Ix nominal + type role UArray nominal nominal When deriving the instance for (IArray UArray N) RolesIArray.hs:10:13: - Could not coerce from ‘UArray i Word64’ to ‘UArray i N’ - because the second type argument of ‘UArray’ has role Nominal, - but the arguments ‘Word64’ and ‘N’ differ - arising from the coercion of the method ‘bounds’ - from type ‘forall i. Ix i => UArray i Word64 -> (i, i)’ - to type ‘forall i. Ix i => UArray i N -> (i, i)’ - Possible fix: - use a standalone 'deriving instance' declaration, - so you can specify the instance context yourself + Couldn't match type ‘Word64’ with ‘N’ + arising from the coercion of the method ‘bounds’ + from type ‘forall i. Ix i => UArray i Word64 -> (i, i)’ + to type ‘forall i. Ix i => UArray i N -> (i, i)’ + Relevant role signatures: + type role Ix nominal + type role (,) representational representational + type role UArray nominal nominal When deriving the instance for (IArray UArray N) diff --git a/testsuite/tests/typecheck/should_compile/T9117_3.hs b/testsuite/tests/typecheck/should_compile/T9117_3.hs new file mode 100644 index 0000000000..64db035872 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T9117_3.hs @@ -0,0 +1,7 @@ +module T9117_3 where + +import Data.Type.Coercion +import Data.Coerce + +eta :: Coercible f g => Coercion (f a) (g a) +eta = Coercion diff --git a/testsuite/tests/typecheck/should_compile/T9708.hs b/testsuite/tests/typecheck/should_compile/T9708.hs index b170ef3b6d..61928d41ad 100644 --- a/testsuite/tests/typecheck/should_compile/T9708.hs +++ b/testsuite/tests/typecheck/should_compile/T9708.hs @@ -7,7 +7,14 @@ import Data.Proxy type family SomeFun (n :: Nat) -- See the Trac ticket; whether this suceeds or fails is distintly random --- Currently it succeeds + +-- upon creation, commit f861fc6ad8e5504a4fecfc9bb0945fe2d313687c, this failed + +-- with Simon's optimization to the flattening algorithm, commit +-- 37b3646c9da4da62ae95aa3a9152335e485b261e, this succeeded + +-- with the change to stop Deriveds from rewriting Deriveds (around Dec. 12, 2014), +-- this failed again ti7 :: (x <= y, y <= x) => Proxy (SomeFun x) -> Proxy y -> () ti7 _ _ = () diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 72c2e6688e..7d33ad580c 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -423,8 +423,9 @@ test('MutRec', normal, compile, ['']) test('T8856', normal, compile, ['']) test('T9569a', normal, compile, ['']) test('T9117', normal, compile, ['']) -test('T9117_2', expect_broken('9117'), compile, ['']) -test('T9708', normal, compile, ['']) +test('T9117_2', normal, compile, ['']) +test('T9117_3', normal, compile, ['']) +test('T9708', expect_broken(9708), compile, ['']) test('T9404', normal, compile, ['']) test('T9404b', normal, compile, ['']) test('T7220', normal, compile, ['']) diff --git a/testsuite/tests/typecheck/should_fail/TcCoercibleFail.hs b/testsuite/tests/typecheck/should_fail/TcCoercibleFail.hs index 0431eee184..c102da5cf8 100644 --- a/testsuite/tests/typecheck/should_fail/TcCoercibleFail.hs +++ b/testsuite/tests/typecheck/should_fail/TcCoercibleFail.hs @@ -20,10 +20,8 @@ foo4 = coerce $ one :: Down Int newtype Void = Void Void foo5 = coerce :: Void -> () --- Do not test this; fills up memory ---newtype VoidBad a = VoidBad (VoidBad (a,a)) ---foo5 = coerce :: (VoidBad ()) -> () - +newtype VoidBad a = VoidBad (VoidBad (a,a)) +foo5' = coerce :: (VoidBad ()) -> () -- This shoul fail with a context stack overflow newtype Fix f = Fix (f (Fix f)) diff --git a/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr b/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr index b95b4cea67..52d2c25e97 100644 --- a/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr +++ b/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr @@ -1,66 +1,67 @@ TcCoercibleFail.hs:11:8: - Could not coerce from ‘Int’ to ‘()’ - because ‘Int’ - and ‘()’ - are different types. - arising from a use of ‘coerce’ + Couldn't match representation of type ‘()’ with that of ‘Int’ In the expression: coerce In the expression: coerce $ one :: () In an equation for ‘foo1’: foo1 = coerce $ one :: () TcCoercibleFail.hs:14:8: - Could not coerce from ‘m Int’ to ‘m Age’ - because ‘m Int’ - and ‘m Age’ - are different types. - arising from a use of ‘coerce’ - from the context (Monad m) - bound by the type signature for foo2 :: Monad m => m Age - at TcCoercibleFail.hs:13:9-34 + Couldn't match representation of type ‘m Age’ with that of ‘m Int’ + NB: We cannot know what roles the parameters to ‘m’ have; + we must assume that the role is nominal + Relevant bindings include + foo2 :: m Age (bound at TcCoercibleFail.hs:14:1) In the expression: coerce In the expression: coerce $ (return one :: m Int) In an equation for ‘foo2’: foo2 = coerce $ (return one :: m Int) TcCoercibleFail.hs:16:8: - Could not coerce from ‘Map Int ()’ to ‘Map Age ()’ - because the first type argument of ‘Map’ has role Nominal, - but the arguments ‘Int’ and ‘Age’ differ - arising from a use of ‘coerce’ + Couldn't match type ‘Int’ with ‘Age’ + arising from trying to show that the representations of + ‘Map Int ()’ and + ‘Map Age ()’ are the same + Relevant role signatures: type role Map nominal representational In the expression: coerce In the expression: coerce $ Map one () :: Map Age () In an equation for ‘foo3’: foo3 = coerce $ Map one () :: Map Age () TcCoercibleFail.hs:18:8: - Could not coerce from ‘Int’ to ‘Down Int’ - because the data constructor ‘Data.Ord.Down’ + Couldn't match representation of type ‘Down Int’ with that of ‘Int’ + Relevant role signatures: type role Down representational + The data constructor ‘Data.Ord.Down’ of newtype ‘Down’ is not in scope - arising from a use of ‘coerce’ In the expression: coerce In the expression: coerce $ one :: Down Int In an equation for ‘foo4’: foo4 = coerce $ one :: Down Int TcCoercibleFail.hs:21:8: - Context reduction stack overflow; size = 101 - Use -fcontext-stack=N to increase stack size to N - Coercible Void () + Couldn't match representation of type ‘()’ with that of ‘Void’ In the expression: coerce :: Void -> () In an equation for ‘foo5’: foo5 = coerce :: Void -> () -TcCoercibleFail.hs:30:8: +TcCoercibleFail.hs:24:9: + Couldn't match representation of type ‘()’ + with that of ‘VoidBad ()’ + Relevant role signatures: type role VoidBad phantom + In the expression: coerce :: (VoidBad ()) -> () + In an equation for ‘foo5'’: foo5' = coerce :: (VoidBad ()) -> () + +TcCoercibleFail.hs:28:8: Context reduction stack overflow; size = 101 Use -fcontext-stack=N to increase stack size to N - Coercible - (Either Int (Fix (Either Int))) (Either Age (Fix (Either Age))) + Coercible (Fix (Either Int)) (Fix (Either Age)) In the expression: coerce :: Fix (Either Int) -> Fix (Either Age) In an equation for ‘foo6’: foo6 = coerce :: Fix (Either Int) -> Fix (Either Age) -TcCoercibleFail.hs:31:8: - Could not coerce from ‘Either Int (Fix (Either Int))’ to ‘()’ - because ‘Either Int (Fix (Either Int))’ - and ‘()’ - are different types. - arising from a use of ‘coerce’ +TcCoercibleFail.hs:29:8: + Couldn't match representation of type ‘()’ + with that of ‘Either Int (Fix (Either Int))’ + arising from trying to show that the representations of + ‘Fix (Either Int)’ and + ‘()’ are the same + Relevant role signatures: + type role Either representational representational + type role Fix nominal In the expression: coerce :: Fix (Either Int) -> () In an equation for ‘foo7’: foo7 = coerce :: Fix (Either Int) -> () diff --git a/testsuite/tests/typecheck/should_fail/TcCoercibleFail3.stderr b/testsuite/tests/typecheck/should_fail/TcCoercibleFail3.stderr index 619e81fdfb..797451d3bf 100644 --- a/testsuite/tests/typecheck/should_fail/TcCoercibleFail3.stderr +++ b/testsuite/tests/typecheck/should_fail/TcCoercibleFail3.stderr @@ -1,7 +1,12 @@ TcCoercibleFail3.hs:12:7: - Could not coerce from ‘NT1’ to ‘NT2’ - because ‘NT1’ and ‘NT2’ are different types. - arising from a use of ‘coerce’ + Couldn't match representation of type ‘NT2’ with that of ‘NT1’ + arising from trying to show that the representations of + ‘T NT1’ and + ‘T NT2’ are the same + Relevant role signatures: + type role NT2 representational + type role NT1 representational + type role T representational In the expression: coerce In an equation for ‘foo’: foo = coerce diff --git a/testsuite/tests/typecheck/should_run/TcCoercible.hs b/testsuite/tests/typecheck/should_run/TcCoercible.hs index 284984029f..041456f01f 100644 --- a/testsuite/tests/typecheck/should_run/TcCoercible.hs +++ b/testsuite/tests/typecheck/should_run/TcCoercible.hs @@ -28,9 +28,11 @@ deriving instance Show (f (Fix f)) => Show (Fix f) -- This ensures that explicitly given constraints are consulted, even -- at higher depths -data Oracle where Oracle :: Coercible (Fix (Either Age)) (Fix (Either Int)) => Oracle -foo :: Oracle -> Either Age (Fix (Either Age)) -> Fix (Either Int) -foo Oracle = coerce +-- This stopped working with the fix to #9117 +--data Oracle where Oracle :: Coercible (Fix (Either Age)) +-- (Fix (Either Int)) => Oracle +--foo :: Oracle -> Either Age (Fix (Either Age)) -> Fix (Either Int) +--foo Oracle = coerce -- This ensures that Coercible looks into newtype instances (#8548) data family Fam k @@ -60,13 +62,14 @@ main = do print (coerce $ (Fix (Left ()) :: Fix (Either ())) :: Either () (Fix (Either ()))) print (coerce $ (Left () :: Either () (Fix (Either ()))) :: Fix (Either ())) - -- print (coerce $ (FixEither (Left age) :: FixEither Age) :: Either Int (FixEither Int)) - -- print (coerce $ (Left one :: Either Int (FixEither Age)) :: FixEither Age) +-- print (coerce $ (FixEither (Left age) :: FixEither Age) +-- :: Either Int (FixEither Int)) +-- print (coerce $ (Left one :: Either Int (FixEither Age)) :: FixEither Age) print (coerce $ True :: Fam Int) print (coerce $ FamInt True :: Bool) - foo `seq` return () +-- foo `seq` return () where one = 1 :: Int |