Commit 0cc47eb9 authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Rewrite `Coercible` solver

Summary:
This is a rewrite of the algorithm to solve for Coercible "instances".

A preliminary form of these ideas is at
https://ghc.haskell.org/trac/ghc/wiki/Design/NewCoercibleSolver

The basic idea here is that the `EqPred` constructor of `PredTree`
now is parameterised by a new type `EqRel` (where
`data EqRel = NomEq | ReprEq`). Thus, every equality constraint can
now talk about nominal equality (the usual case) or representational
equality (the `Coercible` case).

This is a change from the previous
behavior where `Coercible` was just considered a regular class with
a special case in `matchClassInst`.

Because of this change, representational equalities are now
canonicalized just like nominal ones, allowing more equalities
to be solved -- in particular, the case at the top of #9117.

A knock-on effect is that the flattener must be aware of the
choice of equality relation, because the inert set now stores
both representational inert equalities alongside the nominal
inert equalities. Of course, we can use representational equalities
to rewrite only within another representational equality --
thus the parameterization of the flattener.

A nice side effect of this change is that I've introduced a new
type `CtFlavour`, which tracks G vs. W vs. D, removing some ugliness
in the flattener.

This commit includes some refactoring as discussed on D546.
It also removes the ability of Deriveds to rewrite Deriveds.

This fixes bugs #9117 and #8984.

Reviewers: simonpj, austin, nomeata

Subscribers: carter, thomie

Differential Revision: https://phabricator.haskell.org/D546

GHC Trac Issues: #9117, #8984
parent 058262ba
......@@ -971,7 +971,7 @@ dataConCannotMatch tys con
-- TODO: could gather equalities from superclasses too
predEqs pred = case classifyPredType pred of
EqPred ty1 ty2 -> [(ty1, ty2)]
EqPred NomEq ty1 ty2 -> [(ty1, ty2)]
TuplePred ts -> concatMap predEqs ts
_ -> []
......
......@@ -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)
......
......@@ -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
{-
************************************************************************
* *
......
......@@ -480,7 +480,7 @@ 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])]
EqPred NomEq t1 t2 -> [([t1],[t2]), ([t2],[t1])]
TuplePred ts -> concatMap determined ts
_ -> []
......
......@@ -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 ()
......
......@@ -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
EqPred eq_rel ty1 ty2 -> canEqNC new_ev eq_rel ty1 ty2
_ -> continueWith $
CIrredEvCan { cc_ev = new_ev } } } }
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
; 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" }
Stop ev s -> return (Stop ev s) } -- Found a cached copy; won't happen
; 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
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)
can_eq_wanted_app :: CtEvidence -> TcType -> TcType
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