diff options
Diffstat (limited to 'compiler/GHC/Tc/Solver/Canonical.hs')
| -rw-r--r-- | compiler/GHC/Tc/Solver/Canonical.hs | 112 |
1 files changed, 67 insertions, 45 deletions
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs index 4e828c919c..2fc8664450 100644 --- a/compiler/GHC/Tc/Solver/Canonical.hs +++ b/compiler/GHC/Tc/Solver/Canonical.hs @@ -904,22 +904,23 @@ It is conceivable to do a better job at tracking whether or not a type is flattened, but this is left as future work. (Mar '15) -Note [FunTy and decomposing tycon applications] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When can_eq_nc' attempts to decompose a tycon application we haven't yet zonked. -This means that we may very well have a FunTy containing a type of some unknown -kind. For instance, we may have, +Note [Decomposing FunTy] +~~~~~~~~~~~~~~~~~~~~~~~~ +can_eq_nc' may attempt to decompose a FunTy that is un-zonked. This +means that we may very well have a FunTy containing a type of some +unknown kind. For instance, we may have, FunTy (a :: k) Int -Where k is a unification variable. tcRepSplitTyConApp_maybe panics in the event -that it sees such a type as it cannot determine the RuntimeReps which the (->) -is applied to. Consequently, it is vital that we instead use -tcRepSplitTyConApp_maybe', which simply returns Nothing in such a case. - -When this happens can_eq_nc' will fail to decompose, zonk, and try again. +Where k is a unification variable. So the calls to getRuntimeRep_maybe may +fail (returning Nothing). In that case we'll fall through, zonk, and try again. Zonking should fill the variable k, meaning that decomposition will succeed the second time around. + +Also note that we require the AnonArgFlag to match. This will stop +us decomposing + (Int -> Bool) ~ (Show a => blah) +It's as if we treat (->) and (=>) as different type constructors. -} canEqNC :: CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct) @@ -1003,13 +1004,26 @@ can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _ = do { setEvBindIfWanted ev (evCoercion $ mkReflCo (eqRelRole eq_rel) ty1) ; stopWith ev "Equal LitTy" } --- Try to decompose type constructor applications --- Including FunTy (s -> t) -can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1 _ ty2 _ - --- See Note [FunTy and decomposing type constructor applications]. - | Just (tc1, tys1) <- repSplitTyConApp_maybe ty1 - , Just (tc2, tys2) <- repSplitTyConApp_maybe ty2 - , not (isTypeFamilyTyCon tc1) +-- Decompose FunTy: (s -> t) and (c => t) +-- NB: don't decompose (Int -> blah) ~ (Show a => blah) +can_eq_nc' _flat _rdr_env _envs ev eq_rel + (FunTy { ft_af = af1, ft_arg = ty1a, ft_res = ty1b }) _ + (FunTy { ft_af = af2, ft_arg = ty2a, ft_res = ty2b }) _ + | af1 == af2 -- Don't decompose (Int -> blah) ~ (Show a => blah) + , Just ty1a_rep <- getRuntimeRep_maybe ty1a -- getRutimeRep_maybe: + , Just ty1b_rep <- getRuntimeRep_maybe ty1b -- see Note [Decomposing FunTy] + , Just ty2a_rep <- getRuntimeRep_maybe ty2a + , Just ty2b_rep <- getRuntimeRep_maybe ty2b + = canDecomposableTyConAppOK ev eq_rel funTyCon + [ty1a_rep, ty1b_rep, ty1a, ty1b] + [ty2a_rep, ty2b_rep, ty2a, ty2b] + +-- Decompose type constructor applications +-- NB: e have expanded type synonyms already +can_eq_nc' _flat _rdr_env _envs ev eq_rel + (TyConApp tc1 tys1) _ + (TyConApp tc2 tys2) _ + | not (isTypeFamilyTyCon tc1) , not (isTypeFamilyTyCon tc2) = canTyConApp ev eq_rel tc1 tys1 tc2 tys2 @@ -1452,15 +1466,13 @@ canTyConApp :: CtEvidence -> EqRel -> TyCon -> [TcType] -> TcS (StopOrContinue Ct) -- See Note [Decomposing TyConApps] +-- Neither tc1 nor tc2 is a saturated funTyCon canTyConApp ev eq_rel tc1 tys1 tc2 tys2 | tc1 == tc2 , tys1 `equalLength` tys2 = do { inerts <- getTcSInerts ; if can_decompose inerts - then do { traceTcS "canTyConApp" - (ppr ev $$ ppr eq_rel $$ ppr tc1 $$ ppr tys1 $$ ppr tys2) - ; canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2 - ; stopWith ev "Decomposed TyConApp" } + then canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2 else canEqFailure ev eq_rel ty1 ty2 } -- See Note [Skolem abstract data] (at tyConSkolem) @@ -1476,6 +1488,10 @@ canTyConApp ev eq_rel tc1 tys1 tc2 tys2 | otherwise = canEqHardFailure ev ty1 ty2 where + -- Reconstruct the types for error messages. This would do + -- the wrong thing (from a pretty printing point of view) + -- for functions, because we've lost the AnonArgFlag; but + -- in fact we never call canTyConApp on a saturated FunTyCon ty1 = mkTyConApp tc1 tys1 ty2 = mkTyConApp tc2 tys2 @@ -1673,30 +1689,35 @@ Conclusion: canDecomposableTyConAppOK :: CtEvidence -> EqRel -> TyCon -> [TcType] -> [TcType] - -> TcS () + -> TcS (StopOrContinue Ct) -- Precondition: tys1 and tys2 are the same length, hence "OK" canDecomposableTyConAppOK ev eq_rel tc tys1 tys2 = ASSERT( tys1 `equalLength` tys2 ) - case ev of - CtDerived {} - -> unifyDeriveds loc tc_roles tys1 tys2 - - CtWanted { ctev_dest = dest } - -- new_locs and tc_roles are both infinite, so - -- we are guaranteed that cos has the same length - -- as tys1 and tys2 - -> do { cos <- zipWith4M unifyWanted new_locs tc_roles tys1 tys2 - ; setWantedEq dest (mkTyConAppCo role tc cos) } - - CtGiven { ctev_evar = evar } - -> do { let ev_co = mkCoVarCo evar - ; given_evs <- newGivenEvVars loc $ - [ ( mkPrimEqPredRole r ty1 ty2 - , evCoercion $ mkNthCo r i ev_co ) - | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..] - , r /= Phantom - , not (isCoercionTy ty1) && not (isCoercionTy ty2) ] - ; emitWorkNC given_evs } + do { traceTcS "canDecomposableTyConAppOK" + (ppr ev $$ ppr eq_rel $$ ppr tc $$ ppr tys1 $$ ppr tys2) + ; case ev of + CtDerived {} + -> unifyDeriveds loc tc_roles tys1 tys2 + + CtWanted { ctev_dest = dest } + -- new_locs and tc_roles are both infinite, so + -- we are guaranteed that cos has the same length + -- as tys1 and tys2 + -> do { cos <- zipWith4M unifyWanted new_locs tc_roles tys1 tys2 + ; setWantedEq dest (mkTyConAppCo role tc cos) } + + CtGiven { ctev_evar = evar } + -> do { let ev_co = mkCoVarCo evar + ; given_evs <- newGivenEvVars loc $ + [ ( mkPrimEqPredRole r ty1 ty2 + , evCoercion $ mkNthCo r i ev_co ) + | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..] + , r /= Phantom + , not (isCoercionTy ty1) && not (isCoercionTy ty2) ] + ; emitWorkNC given_evs } + + ; stopWith ev "Decomposed TyConApp" } + where loc = ctEvLoc ev role = eqRelRole eq_rel @@ -1747,7 +1768,8 @@ canEqHardFailure :: CtEvidence -> TcType -> TcType -> TcS (StopOrContinue Ct) -- See Note [Make sure that insolubles are fully rewritten] canEqHardFailure ev ty1 ty2 - = do { (s1, co1) <- flatten FM_SubstOnly ev ty1 + = do { traceTcS "canEqHardFailure" (ppr ty1 $$ ppr ty2) + ; (s1, co1) <- flatten FM_SubstOnly ev ty1 ; (s2, co2) <- flatten FM_SubstOnly ev ty2 ; new_ev <- rewriteEqEvidence ev NotSwapped s1 s2 co1 co2 ; continueWith (mkIrredCt InsolubleCIS new_ev) } @@ -2007,7 +2029,7 @@ canEqTyVarHomo ev eq_rel swapped tv1 ps_xi1 xi2 _ -- this guarantees (TyEq:TV) | Just (tv2, co2) <- tcGetCastedTyVar_maybe xi2 - , swapOverTyVars tv1 tv2 + , swapOverTyVars (isGiven ev) tv1 tv2 = do { traceTcS "canEqTyVar swapOver" (ppr tv1 $$ ppr tv2 $$ ppr swapped) ; let role = eqRelRole eq_rel sym_co2 = mkTcSymCo co2 |