diff options
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 |