{-# LANGUAGE CPP #-}
{-# LANGUAGE MultiWayIf #-}
module GHC.Tc.Solver.Equality(
solveEquality
) where
import GHC.Prelude
import GHC.Tc.Solver.Irred( solveIrred )
import GHC.Tc.Solver.Dict( matchLocalInst, chooseInstance )
import GHC.Tc.Solver.Rewrite
import GHC.Tc.Solver.Monad
import GHC.Tc.Solver.InertSet
import GHC.Tc.Solver.Types( findFunEqsByTyCon )
import GHC.Tc.Types.Evidence
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.CtLoc
import GHC.Tc.Types.Origin
import GHC.Tc.Utils.Unify
import GHC.Tc.Utils.TcType
import GHC.Tc.Instance.Family ( tcTopNormaliseNewTypeTF_maybe )
import GHC.Tc.Instance.FunDeps( FunDepEqn(..) )
import qualified GHC.Tc.Utils.Monad as TcM
import GHC.Core.Type
import GHC.Core.Predicate
import GHC.Core.Class
import GHC.Core.DataCon ( dataConName )
import GHC.Core.TyCon
import GHC.Core.TyCo.Rep
import GHC.Core.Coercion
import GHC.Core.Coercion.Axiom
import GHC.Core.Reduction
import GHC.Core.Unify( tcUnifyTyWithTFs )
import GHC.Core.FamInstEnv ( FamInstEnvs, FamInst(..), apartnessCheck
, lookupFamInstEnvByTyCon )
import GHC.Core
import GHC.Types.Var
import GHC.Types.Var.Env
import GHC.Types.Var.Set( anyVarSet )
import GHC.Types.Name.Reader
import GHC.Types.Basic
import GHC.Builtin.Types.Literals ( tryInteractTopFam, tryInteractInertFam )
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Misc
import GHC.Utils.Monad
import GHC.Data.Pair
import GHC.Data.Bag
import Control.Monad
import Data.Maybe ( isJust, isNothing )
import Data.List ( zip4 )
import qualified Data.Semigroup as S
import Data.Bifunctor ( bimap )
import Data.Void( Void )
solveEquality :: CtEvidence -> EqRel -> Type -> Type
-> SolverStage Void
solveEquality :: CtEvidence -> EqRel -> TcType -> TcType -> SolverStage Void
solveEquality CtEvidence
ev EqRel
eq_rel TcType
ty1 TcType
ty2
= do { Pair ty1' ty2' <- CtEvidence -> EqRel -> TcType -> TcType -> SolverStage TypeEqn
zonkEqTypes CtEvidence
ev EqRel
eq_rel TcType
ty1 TcType
ty2
; mb_canon <- canonicaliseEquality ev eq_rel ty1' ty2'
; case mb_canon of {
Left IrredCt
irred_ct -> do { IrredCt -> SolverStage ()
tryQCsIrredEqCt IrredCt
irred_ct
; IrredCt -> SolverStage Void
solveIrred IrredCt
irred_ct } ;
Right EqCt
eq_ct -> do { EqCt -> SolverStage ()
tryInertEqs EqCt
eq_ct
; EqRel -> EqCt -> SolverStage ()
tryFunDeps EqRel
eq_rel EqCt
eq_ct
; EqCt -> SolverStage ()
tryQCsEqCt EqCt
eq_ct
; TcS () -> SolverStage ()
forall a. TcS a -> SolverStage a
simpleStage (EqCt -> TcS ()
updInertEqs EqCt
eq_ct)
; CtEvidence -> String -> SolverStage Void
forall a. CtEvidence -> String -> SolverStage a
stopWithStage (EqCt -> CtEvidence
eqCtEvidence EqCt
eq_ct) String
"Kept inert EqCt" } } }
updInertEqs :: EqCt -> TcS ()
updInertEqs :: EqCt -> TcS ()
updInertEqs EqCt
eq_ct
= do { KickOutSpec -> CtFlavourRole -> TcS ()
kickOutRewritable (CanEqLHS -> KickOutSpec
KOAfterAdding (EqCt -> CanEqLHS
eqCtLHS EqCt
eq_ct)) (EqCt -> CtFlavourRole
eqCtFlavourRole EqCt
eq_ct)
; tc_lvl <- TcS TcLevel
getTcLevel
; updInertCans (addEqToCans tc_lvl eq_ct) }
zonkEqTypes :: CtEvidence -> EqRel -> TcType -> TcType -> SolverStage (Pair TcType)
zonkEqTypes :: CtEvidence -> EqRel -> TcType -> TcType -> SolverStage TypeEqn
zonkEqTypes CtEvidence
ev EqRel
eq_rel TcType
ty1 TcType
ty2
= TcS (StopOrContinue TypeEqn) -> SolverStage TypeEqn
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue TypeEqn) -> SolverStage TypeEqn)
-> TcS (StopOrContinue TypeEqn) -> SolverStage TypeEqn
forall a b. (a -> b) -> a -> b
$ do { res <- TcType -> TcType -> TcS (Either TypeEqn TcType)
go TcType
ty1 TcType
ty2
; case res of
Left TypeEqn
pair -> TypeEqn -> TcS (StopOrContinue TypeEqn)
forall a. a -> TcS (StopOrContinue a)
continueWith TypeEqn
pair
Right TcType
ty -> CtEvidence -> EqRel -> TcType -> TcS (StopOrContinue TypeEqn)
forall a. CtEvidence -> EqRel -> TcType -> TcS (StopOrContinue a)
canEqReflexive CtEvidence
ev EqRel
eq_rel TcType
ty }
where
go :: TcType -> TcType -> TcS (Either (Pair TcType) TcType)
go :: TcType -> TcType -> TcS (Either TypeEqn TcType)
go (TyVarTy TcTyVar
tv1) (TyVarTy TcTyVar
tv2) = TcTyVar -> TcTyVar -> TcS (Either TypeEqn TcType)
tyvar_tyvar TcTyVar
tv1 TcTyVar
tv2
go (TyVarTy TcTyVar
tv1) TcType
ty2 = SwapFlag -> TcTyVar -> TcType -> TcS (Either TypeEqn TcType)
tyvar SwapFlag
NotSwapped TcTyVar
tv1 TcType
ty2
go TcType
ty1 (TyVarTy TcTyVar
tv2) = SwapFlag -> TcTyVar -> TcType -> TcS (Either TypeEqn TcType)
tyvar SwapFlag
IsSwapped TcTyVar
tv2 TcType
ty1
go (FunTy FunTyFlag
af1 TcType
w1 TcType
arg1 TcType
res1) (FunTy FunTyFlag
af2 TcType
w2 TcType
arg2 TcType
res2)
| FunTyFlag
af1 FunTyFlag -> FunTyFlag -> Bool
forall a. Eq a => a -> a -> Bool
== FunTyFlag
af2
, HasCallStack => TcType -> TcType -> Bool
TcType -> TcType -> Bool
eqType TcType
w1 TcType
w2
= do { res_a <- TcType -> TcType -> TcS (Either TypeEqn TcType)
go TcType
arg1 TcType
arg2
; res_b <- go res1 res2
; return $ combine_rev (FunTy af1 w1) res_b res_a }
go ty1 :: TcType
ty1@(FunTy {}) TcType
ty2 = TcType -> TcType -> TcS (Either TypeEqn TcType)
forall {m :: * -> *} {a} {b}.
Monad m =>
a -> a -> m (Either (Pair a) b)
bale_out TcType
ty1 TcType
ty2
go TcType
ty1 ty2 :: TcType
ty2@(FunTy {}) = TcType -> TcType -> TcS (Either TypeEqn TcType)
forall {m :: * -> *} {a} {b}.
Monad m =>
a -> a -> m (Either (Pair a) b)
bale_out TcType
ty1 TcType
ty2
go TcType
ty1 TcType
ty2
| Just (TyCon
tc1, [TcType]
tys1) <- HasDebugCallStack => TcType -> Maybe (TyCon, [TcType])
TcType -> Maybe (TyCon, [TcType])
splitTyConAppNoView_maybe TcType
ty1
, Just (TyCon
tc2, [TcType]
tys2) <- HasDebugCallStack => TcType -> Maybe (TyCon, [TcType])
TcType -> Maybe (TyCon, [TcType])
splitTyConAppNoView_maybe TcType
ty2
= if TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2 Bool -> Bool -> Bool
&& [TcType]
tys1 [TcType] -> [TcType] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [TcType]
tys2
then TyCon -> [TcType] -> [TcType] -> TcS (Either TypeEqn TcType)
tycon TyCon
tc1 [TcType]
tys1 [TcType]
tys2
else TcType -> TcType -> TcS (Either TypeEqn TcType)
forall {m :: * -> *} {a} {b}.
Monad m =>
a -> a -> m (Either (Pair a) b)
bale_out TcType
ty1 TcType
ty2
go TcType
ty1 TcType
ty2
| Just (TcType
ty1a, TcType
ty1b) <- TcType -> Maybe (TcType, TcType)
tcSplitAppTyNoView_maybe TcType
ty1
, Just (TcType
ty2a, TcType
ty2b) <- TcType -> Maybe (TcType, TcType)
tcSplitAppTyNoView_maybe TcType
ty2
= do { res_a <- TcType -> TcType -> TcS (Either TypeEqn TcType)
go TcType
ty1a TcType
ty2a
; res_b <- go ty1b ty2b
; return $ combine_rev mkAppTy res_b res_a }
go ty1 :: TcType
ty1@(LitTy TyLit
lit1) (LitTy TyLit
lit2)
| TyLit
lit1 TyLit -> TyLit -> Bool
forall a. Eq a => a -> a -> Bool
== TyLit
lit2
= Either TypeEqn TcType -> TcS (Either TypeEqn TcType)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcType -> Either TypeEqn TcType
forall a b. b -> Either a b
Right TcType
ty1)
go TcType
ty1 TcType
ty2 = TcType -> TcType -> TcS (Either TypeEqn TcType)
forall {m :: * -> *} {a} {b}.
Monad m =>
a -> a -> m (Either (Pair a) b)
bale_out TcType
ty1 TcType
ty2
bale_out :: a -> a -> m (Either (Pair a) b)
bale_out a
ty1 a
ty2 = Either (Pair a) b -> m (Either (Pair a) b)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (Pair a) b -> m (Either (Pair a) b))
-> Either (Pair a) b -> m (Either (Pair a) b)
forall a b. (a -> b) -> a -> b
$ Pair a -> Either (Pair a) b
forall a b. a -> Either a b
Left (a -> a -> Pair a
forall a. a -> a -> Pair a
Pair a
ty1 a
ty2)
tyvar :: SwapFlag -> TcTyVar -> TcType
-> TcS (Either (Pair TcType) TcType)
tyvar :: SwapFlag -> TcTyVar -> TcType -> TcS (Either TypeEqn TcType)
tyvar SwapFlag
swapped TcTyVar
tv TcType
ty
= case TcTyVar -> TcTyVarDetails
tcTyVarDetails TcTyVar
tv of
MetaTv { mtv_ref :: TcTyVarDetails -> IORef MetaDetails
mtv_ref = IORef MetaDetails
ref }
-> do { cts <- IORef MetaDetails -> TcS MetaDetails
forall a. TcRef a -> TcS a
readTcRef IORef MetaDetails
ref
; case cts of
MetaDetails
Flexi -> TcS (Either TypeEqn TcType)
give_up
Indirect TcType
ty' -> do { TcTyVar -> TcType -> TcS ()
forall {a} {a}. (Outputable a, Outputable a) => a -> a -> TcS ()
trace_indirect TcTyVar
tv TcType
ty'
; SwapFlag
-> (TcType -> TcType -> TcS (Either TypeEqn TcType))
-> TcType
-> TcType
-> TcS (Either TypeEqn TcType)
forall a b. SwapFlag -> (a -> a -> b) -> a -> a -> b
unSwap SwapFlag
swapped TcType -> TcType -> TcS (Either TypeEqn TcType)
go TcType
ty' TcType
ty } }
TcTyVarDetails
_ -> TcS (Either TypeEqn TcType)
give_up
where
give_up :: TcS (Either TypeEqn TcType)
give_up = Either TypeEqn TcType -> TcS (Either TypeEqn TcType)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either TypeEqn TcType -> TcS (Either TypeEqn TcType))
-> Either TypeEqn TcType -> TcS (Either TypeEqn TcType)
forall a b. (a -> b) -> a -> b
$ TypeEqn -> Either TypeEqn TcType
forall a b. a -> Either a b
Left (TypeEqn -> Either TypeEqn TcType)
-> TypeEqn -> Either TypeEqn TcType
forall a b. (a -> b) -> a -> b
$ SwapFlag
-> (TcType -> TcType -> TypeEqn) -> TcType -> TcType -> TypeEqn
forall a b. SwapFlag -> (a -> a -> b) -> a -> a -> b
unSwap SwapFlag
swapped TcType -> TcType -> TypeEqn
forall a. a -> a -> Pair a
Pair (TcTyVar -> TcType
mkTyVarTy TcTyVar
tv) TcType
ty
tyvar_tyvar :: TcTyVar -> TcTyVar -> TcS (Either TypeEqn TcType)
tyvar_tyvar TcTyVar
tv1 TcTyVar
tv2
| TcTyVar
tv1 TcTyVar -> TcTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TcTyVar
tv2 = Either TypeEqn TcType -> TcS (Either TypeEqn TcType)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcType -> Either TypeEqn TcType
forall a b. b -> Either a b
Right (TcTyVar -> TcType
mkTyVarTy TcTyVar
tv1))
| Bool
otherwise = do { (ty1', progress1) <- TcTyVar -> TcS (TcType, Bool)
quick_zonk TcTyVar
tv1
; (ty2', progress2) <- quick_zonk tv2
; if progress1 || progress2
then go ty1' ty2'
else return $ Left (Pair (TyVarTy tv1) (TyVarTy tv2)) }
trace_indirect :: a -> a -> TcS ()
trace_indirect a
tv a
ty
= String -> SDoc -> TcS ()
traceTcS String
"Following filled tyvar (zonk_eq_types)"
(a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
tv SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
forall doc. IsLine doc => doc
equals SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
ty)
quick_zonk :: TcTyVar -> TcS (TcType, Bool)
quick_zonk TcTyVar
tv = case TcTyVar -> TcTyVarDetails
tcTyVarDetails TcTyVar
tv of
MetaTv { mtv_ref :: TcTyVarDetails -> IORef MetaDetails
mtv_ref = IORef MetaDetails
ref }
-> do { cts <- IORef MetaDetails -> TcS MetaDetails
forall a. TcRef a -> TcS a
readTcRef IORef MetaDetails
ref
; case cts of
MetaDetails
Flexi -> (TcType, Bool) -> TcS (TcType, Bool)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcTyVar -> TcType
TyVarTy TcTyVar
tv, Bool
False)
Indirect TcType
ty' -> do { TcTyVar -> TcType -> TcS ()
forall {a} {a}. (Outputable a, Outputable a) => a -> a -> TcS ()
trace_indirect TcTyVar
tv TcType
ty'
; (TcType, Bool) -> TcS (TcType, Bool)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcType
ty', Bool
True) } }
TcTyVarDetails
_ -> (TcType, Bool) -> TcS (TcType, Bool)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcTyVar -> TcType
TyVarTy TcTyVar
tv, Bool
False)
tycon :: TyCon -> [TcType] -> [TcType]
-> TcS (Either (Pair TcType) TcType)
tycon :: TyCon -> [TcType] -> [TcType] -> TcS (Either TypeEqn TcType)
tycon TyCon
tc [TcType]
tys1 [TcType]
tys2
= do { results <- (TcType -> TcType -> TcS (Either TypeEqn TcType))
-> [TcType] -> [TcType] -> TcS [Either TypeEqn TcType]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM TcType -> TcType -> TcS (Either TypeEqn TcType)
go [TcType]
tys1 [TcType]
tys2
; return $ case combine_results results of
Left Pair [TcType]
tys -> TypeEqn -> Either TypeEqn TcType
forall a b. a -> Either a b
Left (TyCon -> [TcType] -> TcType
mkTyConApp TyCon
tc ([TcType] -> TcType) -> Pair [TcType] -> TypeEqn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair [TcType]
tys)
Right [TcType]
tys -> TcType -> Either TypeEqn TcType
forall a b. b -> Either a b
Right (TyCon -> [TcType] -> TcType
mkTyConApp TyCon
tc [TcType]
tys) }
combine_results :: [Either (Pair TcType) TcType]
-> Either (Pair [TcType]) [TcType]
combine_results :: [Either TypeEqn TcType] -> Either (Pair [TcType]) [TcType]
combine_results = (Pair [TcType] -> Pair [TcType])
-> ([TcType] -> [TcType])
-> Either (Pair [TcType]) [TcType]
-> Either (Pair [TcType]) [TcType]
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (([TcType] -> [TcType]) -> Pair [TcType] -> Pair [TcType]
forall a b. (a -> b) -> Pair a -> Pair b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [TcType] -> [TcType]
forall a. [a] -> [a]
reverse) [TcType] -> [TcType]
forall a. [a] -> [a]
reverse (Either (Pair [TcType]) [TcType]
-> Either (Pair [TcType]) [TcType])
-> ([Either TypeEqn TcType] -> Either (Pair [TcType]) [TcType])
-> [Either TypeEqn TcType]
-> Either (Pair [TcType]) [TcType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
(Either (Pair [TcType]) [TcType]
-> Either TypeEqn TcType -> Either (Pair [TcType]) [TcType])
-> Either (Pair [TcType]) [TcType]
-> [Either TypeEqn TcType]
-> Either (Pair [TcType]) [TcType]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((TcType -> [TcType] -> [TcType])
-> Either (Pair [TcType]) [TcType]
-> Either TypeEqn TcType
-> Either (Pair [TcType]) [TcType]
forall a b c.
(a -> b -> c)
-> Either (Pair b) b -> Either (Pair a) a -> Either (Pair c) c
combine_rev (:)) ([TcType] -> Either (Pair [TcType]) [TcType]
forall a b. b -> Either a b
Right [])
combine_rev :: (a -> b -> c)
-> Either (Pair b) b
-> Either (Pair a) a
-> Either (Pair c) c
combine_rev :: forall a b c.
(a -> b -> c)
-> Either (Pair b) b -> Either (Pair a) a -> Either (Pair c) c
combine_rev a -> b -> c
f (Left Pair b
list) (Left Pair a
elt) = Pair c -> Either (Pair c) c
forall a b. a -> Either a b
Left (a -> b -> c
f (a -> b -> c) -> Pair a -> Pair (b -> c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair a
elt Pair (b -> c) -> Pair b -> Pair c
forall a b. Pair (a -> b) -> Pair a -> Pair b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pair b
list)
combine_rev a -> b -> c
f (Left Pair b
list) (Right a
ty) = Pair c -> Either (Pair c) c
forall a b. a -> Either a b
Left (a -> b -> c
f (a -> b -> c) -> Pair a -> Pair (b -> c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Pair a
forall a. a -> Pair a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
ty Pair (b -> c) -> Pair b -> Pair c
forall a b. Pair (a -> b) -> Pair a -> Pair b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pair b
list)
combine_rev a -> b -> c
f (Right b
tys) (Left Pair a
elt) = Pair c -> Either (Pair c) c
forall a b. a -> Either a b
Left (a -> b -> c
f (a -> b -> c) -> Pair a -> Pair (b -> c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair a
elt Pair (b -> c) -> Pair b -> Pair c
forall a b. Pair (a -> b) -> Pair a -> Pair b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> Pair b
forall a. a -> Pair a
forall (f :: * -> *) a. Applicative f => a -> f a
pure b
tys)
combine_rev a -> b -> c
f (Right b
tys) (Right a
ty) = c -> Either (Pair c) c
forall a b. b -> Either a b
Right (a -> b -> c
f a
ty b
tys)
canonicaliseEquality
:: CtEvidence -> EqRel
-> Type -> Type
-> SolverStage (Either IrredCt EqCt)
canonicaliseEquality :: CtEvidence
-> EqRel -> TcType -> TcType -> SolverStage (Either IrredCt EqCt)
canonicaliseEquality CtEvidence
ev EqRel
eq_rel TcType
ty1 TcType
ty2
= TcS (StopOrContinue (Either IrredCt EqCt))
-> SolverStage (Either IrredCt EqCt)
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue (Either IrredCt EqCt))
-> SolverStage (Either IrredCt EqCt))
-> TcS (StopOrContinue (Either IrredCt EqCt))
-> SolverStage (Either IrredCt EqCt)
forall a b. (a -> b) -> a -> b
$ do { String -> SDoc -> TcS ()
traceTcS String
"canonicaliseEquality" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev, EqRel -> SDoc
forall a. Outputable a => a -> SDoc
ppr EqRel
eq_rel, TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty1, TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty2 ]
; rdr_env <- TcS GlobalRdrEnv
getGlobalRdrEnvTcS
; fam_insts <- getFamInstEnvs
; can_eq_nc False rdr_env fam_insts ev eq_rel ty1 ty1 ty2 ty2 }
can_eq_nc
:: Bool
-> GlobalRdrEnv
-> FamInstEnvs
-> CtEvidence
-> EqRel
-> Type -> Type
-> Type -> Type
-> TcS (StopOrContinue (Either IrredCt EqCt))
can_eq_nc :: Bool
-> GlobalRdrEnv
-> (FamInstEnv, FamInstEnv)
-> CtEvidence
-> EqRel
-> TcType
-> TcType
-> TcType
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
can_eq_nc Bool
_flat GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
eq_rel ty1 :: TcType
ty1@(TyConApp TyCon
tc1 []) TcType
_ps_ty1 (TyConApp TyCon
tc2 []) TcType
_ps_ty2
| TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
= CtEvidence
-> EqRel -> TcType -> TcS (StopOrContinue (Either IrredCt EqCt))
forall a. CtEvidence -> EqRel -> TcType -> TcS (StopOrContinue a)
canEqReflexive CtEvidence
ev EqRel
eq_rel TcType
ty1
can_eq_nc Bool
rewritten GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
envs CtEvidence
ev EqRel
eq_rel TcType
ty1 TcType
ps_ty1 TcType
ty2 TcType
ps_ty2
| Just TcType
ty1' <- TcType -> Maybe TcType
coreView TcType
ty1 = Bool
-> GlobalRdrEnv
-> (FamInstEnv, FamInstEnv)
-> CtEvidence
-> EqRel
-> TcType
-> TcType
-> TcType
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
can_eq_nc Bool
rewritten GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
envs CtEvidence
ev EqRel
eq_rel TcType
ty1' TcType
ps_ty1 TcType
ty2 TcType
ps_ty2
| Just TcType
ty2' <- TcType -> Maybe TcType
coreView TcType
ty2 = Bool
-> GlobalRdrEnv
-> (FamInstEnv, FamInstEnv)
-> CtEvidence
-> EqRel
-> TcType
-> TcType
-> TcType
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
can_eq_nc Bool
rewritten GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
envs CtEvidence
ev EqRel
eq_rel TcType
ty1 TcType
ps_ty1 TcType
ty2' TcType
ps_ty2
can_eq_nc Bool
True GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
ReprEq TcType
ty1 TcType
_ TcType
ty2 TcType
_
| TcType
ty1 HasDebugCallStack => TcType -> TcType -> Bool
TcType -> TcType -> Bool
`tcEqType` TcType
ty2
= CtEvidence
-> EqRel -> TcType -> TcS (StopOrContinue (Either IrredCt EqCt))
forall a. CtEvidence -> EqRel -> TcType -> TcS (StopOrContinue a)
canEqReflexive CtEvidence
ev EqRel
ReprEq TcType
ty1
can_eq_nc Bool
_rewritten GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
envs CtEvidence
ev EqRel
eq_rel TcType
ty1 TcType
ps_ty1 TcType
ty2 TcType
ps_ty2
| EqRel
ReprEq <- EqRel
eq_rel
, Just ((Bag GlobalRdrElt, TcCoercion), TcType)
stuff1 <- (FamInstEnv, FamInstEnv)
-> GlobalRdrEnv
-> TcType
-> Maybe ((Bag GlobalRdrElt, TcCoercion), TcType)
tcTopNormaliseNewTypeTF_maybe (FamInstEnv, FamInstEnv)
envs GlobalRdrEnv
rdr_env TcType
ty1
= GlobalRdrEnv
-> (FamInstEnv, FamInstEnv)
-> CtEvidence
-> SwapFlag
-> TcType
-> ((Bag GlobalRdrElt, TcCoercion), TcType)
-> TcType
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
can_eq_newtype_nc GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
envs CtEvidence
ev SwapFlag
NotSwapped TcType
ty1 ((Bag GlobalRdrElt, TcCoercion), TcType)
stuff1 TcType
ty2 TcType
ps_ty2
| EqRel
ReprEq <- EqRel
eq_rel
, Just ((Bag GlobalRdrElt, TcCoercion), TcType)
stuff2 <- (FamInstEnv, FamInstEnv)
-> GlobalRdrEnv
-> TcType
-> Maybe ((Bag GlobalRdrElt, TcCoercion), TcType)
tcTopNormaliseNewTypeTF_maybe (FamInstEnv, FamInstEnv)
envs GlobalRdrEnv
rdr_env TcType
ty2
= GlobalRdrEnv
-> (FamInstEnv, FamInstEnv)
-> CtEvidence
-> SwapFlag
-> TcType
-> ((Bag GlobalRdrElt, TcCoercion), TcType)
-> TcType
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
can_eq_newtype_nc GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
envs CtEvidence
ev SwapFlag
IsSwapped TcType
ty2 ((Bag GlobalRdrElt, TcCoercion), TcType)
stuff2 TcType
ty1 TcType
ps_ty1
can_eq_nc Bool
rewritten GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
envs CtEvidence
ev EqRel
eq_rel (CastTy TcType
ty1 TcCoercion
co1) TcType
_ TcType
ty2 TcType
ps_ty2
| Maybe CanEqLHS -> Bool
forall a. Maybe a -> Bool
isNothing (TcType -> Maybe CanEqLHS
canEqLHS_maybe TcType
ty2)
= Bool
-> GlobalRdrEnv
-> (FamInstEnv, FamInstEnv)
-> CtEvidence
-> EqRel
-> SwapFlag
-> TcType
-> TcCoercion
-> TcType
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCast Bool
rewritten GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
envs CtEvidence
ev EqRel
eq_rel SwapFlag
NotSwapped TcType
ty1 TcCoercion
co1 TcType
ty2 TcType
ps_ty2
can_eq_nc Bool
rewritten GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
envs CtEvidence
ev EqRel
eq_rel TcType
ty1 TcType
ps_ty1 (CastTy TcType
ty2 TcCoercion
co2) TcType
_
| Maybe CanEqLHS -> Bool
forall a. Maybe a -> Bool
isNothing (TcType -> Maybe CanEqLHS
canEqLHS_maybe TcType
ty1)
= Bool
-> GlobalRdrEnv
-> (FamInstEnv, FamInstEnv)
-> CtEvidence
-> EqRel
-> SwapFlag
-> TcType
-> TcCoercion
-> TcType
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCast Bool
rewritten GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
envs CtEvidence
ev EqRel
eq_rel SwapFlag
IsSwapped TcType
ty2 TcCoercion
co2 TcType
ty1 TcType
ps_ty1
can_eq_nc Bool
_rewritten GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
eq_rel ty1 :: TcType
ty1@(LitTy TyLit
l1) TcType
_ (LitTy TyLit
l2) TcType
_
| TyLit
l1 TyLit -> TyLit -> Bool
forall a. Eq a => a -> a -> Bool
== TyLit
l2
= do { CtEvidence -> CanonicalEvidence -> EvTerm -> TcS ()
setEvBindIfWanted CtEvidence
ev CanonicalEvidence
EvCanonical (TcCoercion -> EvTerm
evCoercion (TcCoercion -> EvTerm) -> TcCoercion -> EvTerm
forall a b. (a -> b) -> a -> b
$ Role -> TcType -> TcCoercion
mkReflCo (EqRel -> Role
eqRelRole EqRel
eq_rel) TcType
ty1)
; CtEvidence -> String -> TcS (StopOrContinue (Either IrredCt EqCt))
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Equal LitTy" }
can_eq_nc Bool
_rewritten GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
eq_rel
ty1 :: TcType
ty1@(FunTy { ft_mult :: TcType -> TcType
ft_mult = TcType
am1, ft_af :: TcType -> FunTyFlag
ft_af = FunTyFlag
af1, ft_arg :: TcType -> TcType
ft_arg = TcType
ty1a, ft_res :: TcType -> TcType
ft_res = TcType
ty1b }) TcType
_ps_ty1
ty2 :: TcType
ty2@(FunTy { ft_mult :: TcType -> TcType
ft_mult = TcType
am2, ft_af :: TcType -> FunTyFlag
ft_af = FunTyFlag
af2, ft_arg :: TcType -> TcType
ft_arg = TcType
ty2a, ft_res :: TcType -> TcType
ft_res = TcType
ty2b }) TcType
_ps_ty2
| FunTyFlag
af1 FunTyFlag -> FunTyFlag -> Bool
forall a. Eq a => a -> a -> Bool
== FunTyFlag
af2
= CtEvidence
-> EqRel
-> FunTyFlag
-> (TcType, TcType, TcType, TcType)
-> (TcType, TcType, TcType, TcType)
-> TcS (StopOrContinue (Either IrredCt EqCt))
forall a.
CtEvidence
-> EqRel
-> FunTyFlag
-> (TcType, TcType, TcType, TcType)
-> (TcType, TcType, TcType, TcType)
-> TcS (StopOrContinue a)
canDecomposableFunTy CtEvidence
ev EqRel
eq_rel FunTyFlag
af1 (TcType
ty1,TcType
am1,TcType
ty1a,TcType
ty1b) (TcType
ty2,TcType
am2,TcType
ty2a,TcType
ty2b)
can_eq_nc Bool
rewritten GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
eq_rel TcType
ty1 TcType
_ TcType
ty2 TcType
_
| Just (TyCon
tc1, [TcType]
tys1) <- HasDebugCallStack => TcType -> Maybe (TyCon, [TcType])
TcType -> Maybe (TyCon, [TcType])
tcSplitTyConApp_maybe TcType
ty1
, Just (TyCon
tc2, [TcType]
tys2) <- HasDebugCallStack => TcType -> Maybe (TyCon, [TcType])
TcType -> Maybe (TyCon, [TcType])
tcSplitTyConApp_maybe TcType
ty2
, Bool -> Bool
not (TyCon -> Bool
isTypeFamilyTyCon TyCon
tc1 Bool -> Bool -> Bool
|| TyCon -> Bool
isTypeFamilyTyCon TyCon
tc2)
, let role :: Role
role = EqRel -> Role
eqRelRole EqRel
eq_rel
both_generative :: Bool
both_generative = TyCon -> Role -> Bool
isGenerativeTyCon TyCon
tc1 Role
role Bool -> Bool -> Bool
&& TyCon -> Role -> Bool
isGenerativeTyCon TyCon
tc2 Role
role
, Bool
rewritten Bool -> Bool -> Bool
|| Bool
both_generative
= CtEvidence
-> EqRel
-> Bool
-> (TcType, TyCon, [TcType])
-> (TcType, TyCon, [TcType])
-> TcS (StopOrContinue (Either IrredCt EqCt))
canTyConApp CtEvidence
ev EqRel
eq_rel Bool
both_generative (TcType
ty1,TyCon
tc1,[TcType]
tys1) (TcType
ty2,TyCon
tc2,[TcType]
tys2)
can_eq_nc Bool
_rewritten GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
eq_rel
s1 :: TcType
s1@ForAllTy{} TcType
_
s2 :: TcType
s2@ForAllTy{} TcType
_
= CtEvidence
-> EqRel
-> TcType
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
can_eq_nc_forall CtEvidence
ev EqRel
eq_rel TcType
s1 TcType
s2
can_eq_nc Bool
True GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
NomEq TcType
ty1 TcType
_ TcType
ty2 TcType
_
| Just (TcType
t1, TcType
s1) <- TcType -> Maybe (TcType, TcType)
tcSplitAppTy_maybe TcType
ty1
, Just (TcType
t2, TcType
s2) <- TcType -> Maybe (TcType, TcType)
tcSplitAppTy_maybe TcType
ty2
= CtEvidence
-> TcType
-> TcType
-> TcType
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
can_eq_app CtEvidence
ev TcType
t1 TcType
s1 TcType
t2 TcType
s2
can_eq_nc Bool
False GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
envs CtEvidence
ev EqRel
eq_rel TcType
_ TcType
ps_ty1 TcType
_ TcType
ps_ty2
=
do { (redn1@(Reduction _ xi1), rewriters1) <- CtEvidence -> TcType -> TcS (Reduction, RewriterSet)
rewrite CtEvidence
ev TcType
ps_ty1
; (redn2@(Reduction _ xi2), rewriters2) <- rewrite ev ps_ty2
; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped redn1 redn2
; traceTcS "can_eq_nc: go round again" (ppr new_ev $$ ppr xi1 $$ ppr xi2)
; can_eq_nc True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
can_eq_nc Bool
True GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
eq_rel TcType
ty1 TcType
ps_ty1 TcType
ty2 TcType
ps_ty2
| Just CanEqLHS
can_eq_lhs1 <- TcType -> Maybe CanEqLHS
canEqLHS_maybe TcType
ty1
= do { String -> SDoc -> TcS ()
traceTcS String
"can_eq1" (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty1 SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty2)
; CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> TcType
-> TcType
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCanLHS CtEvidence
ev EqRel
eq_rel SwapFlag
NotSwapped CanEqLHS
can_eq_lhs1 TcType
ps_ty1 TcType
ty2 TcType
ps_ty2 }
| Just CanEqLHS
can_eq_lhs2 <- TcType -> Maybe CanEqLHS
canEqLHS_maybe TcType
ty2
= do { String -> SDoc -> TcS ()
traceTcS String
"can_eq2" (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty1 SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty2)
; CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> TcType
-> TcType
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCanLHS CtEvidence
ev EqRel
eq_rel SwapFlag
IsSwapped CanEqLHS
can_eq_lhs2 TcType
ps_ty2 TcType
ty1 TcType
ps_ty1 }
can_eq_nc Bool
True GlobalRdrEnv
_rdr_env (FamInstEnv, FamInstEnv)
_envs CtEvidence
ev EqRel
eq_rel TcType
_ TcType
ps_ty1 TcType
_ TcType
ps_ty2
= do { String -> SDoc -> TcS ()
traceTcS String
"can_eq_nc catch-all case" (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ps_ty1 SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ps_ty2)
; case EqRel
eq_rel of
EqRel
ReprEq -> CtIrredReason
-> CtEvidence -> TcS (StopOrContinue (Either IrredCt EqCt))
forall a.
CtIrredReason
-> CtEvidence -> TcS (StopOrContinue (Either IrredCt a))
finishCanWithIrred CtIrredReason
ReprEqReason CtEvidence
ev
EqRel
NomEq -> CtIrredReason
-> CtEvidence -> TcS (StopOrContinue (Either IrredCt EqCt))
forall a.
CtIrredReason
-> CtEvidence -> TcS (StopOrContinue (Either IrredCt a))
finishCanWithIrred CtIrredReason
ShapeMismatchReason CtEvidence
ev }
can_eq_nc_forall :: CtEvidence -> EqRel
-> Type -> Type
-> TcS (StopOrContinue (Either IrredCt EqCt))
can_eq_nc_forall :: CtEvidence
-> EqRel
-> TcType
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
can_eq_nc_forall CtEvidence
ev EqRel
eq_rel TcType
s1 TcType
s2
| CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
orig_dest } <- CtEvidence
ev
= do { let ([ForAllTyBinder]
bndrs1, TcType
phi1, [ForAllTyBinder]
bndrs2, TcType
phi2) = TcType
-> TcType -> ([ForAllTyBinder], TcType, [ForAllTyBinder], TcType)
split_foralls TcType
s1 TcType
s2
flags1 :: [ForAllTyFlag]
flags1 = [ForAllTyBinder] -> [ForAllTyFlag]
forall tv argf. [VarBndr tv argf] -> [argf]
binderFlags [ForAllTyBinder]
bndrs1
flags2 :: [ForAllTyFlag]
flags2 = [ForAllTyBinder] -> [ForAllTyFlag]
forall tv argf. [VarBndr tv argf] -> [argf]
binderFlags [ForAllTyBinder]
bndrs2
; if EqRel
eq_rel EqRel -> EqRel -> Bool
forall a. Eq a => a -> a -> Bool
== EqRel
NomEq Bool -> Bool -> Bool
&& Bool -> Bool
not ((ForAllTyFlag -> ForAllTyFlag -> Bool)
-> [ForAllTyFlag] -> [ForAllTyFlag] -> Bool
forall a b. (a -> b -> Bool) -> [a] -> [b] -> Bool
all2 ForAllTyFlag -> ForAllTyFlag -> Bool
eqForAllVis [ForAllTyFlag]
flags1 [ForAllTyFlag]
flags2)
then do { String -> SDoc -> TcS ()
traceTcS String
"Forall failure: visibility-mismatch" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
s1, TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
s2, [ForAllTyBinder] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [ForAllTyBinder]
bndrs1, [ForAllTyBinder] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [ForAllTyBinder]
bndrs2
, [ForAllTyFlag] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [ForAllTyFlag]
flags1, [ForAllTyFlag] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [ForAllTyFlag]
flags2 ]
; CtEvidence
-> TcType -> TcType -> TcS (StopOrContinue (Either IrredCt EqCt))
forall a.
CtEvidence
-> TcType -> TcType -> TcS (StopOrContinue (Either IrredCt a))
canEqHardFailure CtEvidence
ev TcType
s1 TcType
s2 }
else do {
String -> SDoc -> TcS ()
traceTcS String
"Creating implication for polytype equality" (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev)
; let free_tvs :: TyCoVarSet
free_tvs = [TcType] -> TyCoVarSet
tyCoVarsOfTypes [TcType
s1,TcType
s2]
empty_subst1 :: Subst
empty_subst1 = InScopeSet -> Subst
mkEmptySubst (InScopeSet -> Subst) -> InScopeSet -> Subst
forall a b. (a -> b) -> a -> b
$ TyCoVarSet -> InScopeSet
mkInScopeSet TyCoVarSet
free_tvs
; skol_info <- SkolemInfoAnon -> TcS SkolemInfo
forall (m :: * -> *). MonadIO m => SkolemInfoAnon -> m SkolemInfo
mkSkolemInfo (TcType -> SkolemInfoAnon
UnifyForAllSkol TcType
phi1)
; (subst1, skol_tvs) <- tcInstSkolTyVarsX skol_info empty_subst1 $
binderVars bndrs1
; let phi1' = HasDebugCallStack => Subst -> TcType -> TcType
Subst -> TcType -> TcType
substTy Subst
subst1 TcType
phi1
go :: UnifyEnv -> [TcTyVar] -> Subst
-> [TyVarBinder] -> [TyVarBinder] -> TcM.TcM TcCoercion
go UnifyEnv
uenv (TcTyVar
skol_tv:[TcTyVar]
skol_tvs) Subst
subst2 (ForAllTyBinder
bndr1:[ForAllTyBinder]
bndrs1) (ForAllTyBinder
bndr2:[ForAllTyBinder]
bndrs2)
= do { let tv2 :: TcTyVar
tv2 = ForAllTyBinder -> TcTyVar
forall tv argf. VarBndr tv argf -> tv
binderVar ForAllTyBinder
bndr2
vis1 :: ForAllTyFlag
vis1 = ForAllTyBinder -> ForAllTyFlag
forall tv argf. VarBndr tv argf -> argf
binderFlag ForAllTyBinder
bndr1
vis2 :: ForAllTyFlag
vis2 = ForAllTyBinder -> ForAllTyFlag
forall tv argf. VarBndr tv argf -> argf
binderFlag ForAllTyBinder
bndr2
; kind_co <- UnifyEnv -> TcType -> TcType -> TcM TcCoercion
uType (UnifyEnv
uenv UnifyEnv -> Role -> UnifyEnv
`setUEnvRole` Role
Nominal)
(TcTyVar -> TcType
tyVarKind TcTyVar
skol_tv)
(HasDebugCallStack => Subst -> TcType -> TcType
Subst -> TcType -> TcType
substTy Subst
subst2 (TcTyVar -> TcType
tyVarKind TcTyVar
tv2))
; let subst2' = Subst -> TcTyVar -> TcType -> Subst
extendTvSubstAndInScope Subst
subst2 TcTyVar
tv2
(TcType -> TcCoercion -> TcType
mkCastTy (TcTyVar -> TcType
mkTyVarTy TcTyVar
skol_tv) TcCoercion
kind_co)
; co <- go uenv skol_tvs subst2' bndrs1 bndrs2
; return (mkNakedForAllCo skol_tv vis1 vis2 kind_co co)}
go UnifyEnv
uenv [] Subst
subst2 [ForAllTyBinder]
bndrs1 [ForAllTyBinder]
bndrs2
= Bool -> TcM TcCoercion -> TcM TcCoercion
forall a. HasCallStack => Bool -> a -> a
assert ([ForAllTyBinder] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ForAllTyBinder]
bndrs1 Bool -> Bool -> Bool
&& [ForAllTyBinder] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ForAllTyBinder]
bndrs2) (TcM TcCoercion -> TcM TcCoercion)
-> TcM TcCoercion -> TcM TcCoercion
forall a b. (a -> b) -> a -> b
$
UnifyEnv -> TcType -> TcType -> TcM TcCoercion
uType UnifyEnv
uenv TcType
phi1' (Subst -> TcType -> TcType
substTyUnchecked Subst
subst2 TcType
phi2)
go UnifyEnv
_ [TcTyVar]
_ Subst
_ [ForAllTyBinder]
_ [ForAllTyBinder]
_ = String -> TcM TcCoercion
forall a. HasCallStack => String -> a
panic String
"can_eq_nc_forall"
init_subst2 = InScopeSet -> Subst
mkEmptySubst (Subst -> InScopeSet
getSubstInScope Subst
subst1)
; (lvl, (all_co, wanteds)) <- pushLevelNoWorkList (ppr skol_info) $
unifyForAllBody ev (eqRelRole eq_rel) $ \UnifyEnv
uenv ->
UnifyEnv
-> [TcTyVar]
-> Subst
-> [ForAllTyBinder]
-> [ForAllTyBinder]
-> TcM TcCoercion
go UnifyEnv
uenv [TcTyVar]
skol_tvs Subst
init_subst2 [ForAllTyBinder]
bndrs1 [ForAllTyBinder]
bndrs2
; emitTvImplicationTcS lvl (getSkolemInfo skol_info) skol_tvs wanteds
; setWantedEq orig_dest all_co
; stopWith ev "Deferred polytype equality" } }
| Bool
otherwise
= do { String -> SDoc -> TcS ()
traceTcS String
"Omitting decomposition of given polytype equality" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
TcType -> TcType -> SDoc
pprEq TcType
s1 TcType
s2
; CtEvidence -> String -> TcS (StopOrContinue (Either IrredCt EqCt))
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Discard given polytype equality" }
where
split_foralls :: TcType -> TcType
-> ( [ForAllTyBinder], TcType
, [ForAllTyBinder], TcType)
split_foralls :: TcType
-> TcType -> ([ForAllTyBinder], TcType, [ForAllTyBinder], TcType)
split_foralls TcType
s1 TcType
s2
| Just (ForAllTyBinder
bndr1, TcType
s1') <- TcType -> Maybe (ForAllTyBinder, TcType)
splitForAllForAllTyBinder_maybe TcType
s1
, Just (ForAllTyBinder
bndr2, TcType
s2') <- TcType -> Maybe (ForAllTyBinder, TcType)
splitForAllForAllTyBinder_maybe TcType
s2
= let !([ForAllTyBinder]
bndrs1, TcType
phi1, [ForAllTyBinder]
bndrs2, TcType
phi2) = TcType
-> TcType -> ([ForAllTyBinder], TcType, [ForAllTyBinder], TcType)
split_foralls TcType
s1' TcType
s2'
in (ForAllTyBinder
bndr1ForAllTyBinder -> [ForAllTyBinder] -> [ForAllTyBinder]
forall a. a -> [a] -> [a]
:[ForAllTyBinder]
bndrs1, TcType
phi1, ForAllTyBinder
bndr2ForAllTyBinder -> [ForAllTyBinder] -> [ForAllTyBinder]
forall a. a -> [a] -> [a]
:[ForAllTyBinder]
bndrs2, TcType
phi2)
split_foralls TcType
s1 TcType
s2 = ([], TcType
s1, [], TcType
s2)
can_eq_newtype_nc :: GlobalRdrEnv -> FamInstEnvs
-> CtEvidence
-> SwapFlag
-> TcType
-> ((Bag GlobalRdrElt, TcCoercion), TcType)
-> TcType
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
can_eq_newtype_nc :: GlobalRdrEnv
-> (FamInstEnv, FamInstEnv)
-> CtEvidence
-> SwapFlag
-> TcType
-> ((Bag GlobalRdrElt, TcCoercion), TcType)
-> TcType
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
can_eq_newtype_nc GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
envs CtEvidence
ev SwapFlag
swapped TcType
ty1 ((Bag GlobalRdrElt
gres, TcCoercion
co1), TcType
ty1') TcType
ty2 TcType
ps_ty2
= do { String -> SDoc -> TcS ()
traceTcS String
"can_eq_newtype_nc" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev, SwapFlag -> SDoc
forall a. Outputable a => a -> SDoc
ppr SwapFlag
swapped, TcCoercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcCoercion
co1, Bag GlobalRdrElt -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bag GlobalRdrElt
gres, TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty1', TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty2 ]
; let loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
ev' :: CtEvidence
ev' = CtEvidence
ev CtEvidence -> CtLoc -> CtEvidence
`setCtEvLoc` CtLoc -> CtLoc
bumpCtLocDepth CtLoc
loc
; CtLoc -> TcType -> TcS ()
checkReductionDepth CtLoc
loc TcType
ty1
; Bag GlobalRdrElt -> TcS ()
recordUsedGREs Bag GlobalRdrElt
gres
; let redn1 :: Reduction
redn1 = TcCoercion -> TcType -> Reduction
mkReduction TcCoercion
co1 TcType
ty1'
; new_ev <- RewriterSet
-> CtEvidence
-> SwapFlag
-> Reduction
-> Reduction
-> TcS CtEvidence
rewriteEqEvidence RewriterSet
emptyRewriterSet CtEvidence
ev' SwapFlag
swapped
Reduction
redn1 (Role -> TcType -> Reduction
mkReflRedn Role
Representational TcType
ps_ty2)
; can_eq_nc False rdr_env envs new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
can_eq_app :: CtEvidence
-> Xi -> Xi
-> Xi -> Xi
-> TcS (StopOrContinue (Either IrredCt EqCt))
can_eq_app :: CtEvidence
-> TcType
-> TcType
-> TcType
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
can_eq_app CtEvidence
ev TcType
s1 TcType
t1 TcType
s2 TcType
t2
| CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest } <- CtEvidence
ev
= do { String -> SDoc -> TcS ()
traceTcS String
"can_eq_app" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"s1:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
s1, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"t1:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
t1
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"s2:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
s2, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"t2:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
t2
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"vis:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TcType -> Bool
isNextArgVisible TcType
s1) ])
; (co,_,_) <- CtEvidence
-> Role
-> (UnifyEnv -> TcM TcCoercion)
-> TcS (TcCoercion, Cts, [TcTyVar])
forall a.
CtEvidence
-> Role -> (UnifyEnv -> TcM a) -> TcS (a, Cts, [TcTyVar])
wrapUnifierTcS CtEvidence
ev Role
Nominal ((UnifyEnv -> TcM TcCoercion) -> TcS (TcCoercion, Cts, [TcTyVar]))
-> (UnifyEnv -> TcM TcCoercion) -> TcS (TcCoercion, Cts, [TcTyVar])
forall a b. (a -> b) -> a -> b
$ \UnifyEnv
uenv ->
do { let arg_env :: UnifyEnv
arg_env = UnifyEnv -> (CtLoc -> CtLoc) -> UnifyEnv
updUEnvLoc UnifyEnv
uenv (Bool -> Bool -> CtLoc -> CtLoc
adjustCtLoc (TcType -> Bool
isNextArgVisible TcType
s1) Bool
False)
; co_t <- UnifyEnv -> TcType -> TcType -> TcM TcCoercion
uType UnifyEnv
arg_env TcType
t1 TcType
t2
; co_s <- uType uenv s1 s2
; return (mkAppCo co_s co_t) }
; setWantedEq dest co
; stopWith ev "Decomposed [W] AppTy" }
| TcType
s1k TcType -> TcType -> Bool
`mismatches` TcType
s2k
= CtEvidence
-> TcType -> TcType -> TcS (StopOrContinue (Either IrredCt EqCt))
forall a.
CtEvidence
-> TcType -> TcType -> TcS (StopOrContinue (Either IrredCt a))
canEqHardFailure CtEvidence
ev (TcType
s1 TcType -> TcType -> TcType
`mkAppTy` TcType
t1) (TcType
s2 TcType -> TcType -> TcType
`mkAppTy` TcType
t2)
| CtGiven { ctev_evar :: CtEvidence -> TcTyVar
ctev_evar = TcTyVar
evar } <- CtEvidence
ev
= do { let co :: TcCoercion
co = TcTyVar -> TcCoercion
mkCoVarCo TcTyVar
evar
co_s :: TcCoercion
co_s = LeftOrRight -> TcCoercion -> TcCoercion
mkLRCo LeftOrRight
CLeft TcCoercion
co
co_t :: TcCoercion
co_t = LeftOrRight -> TcCoercion -> TcCoercion
mkLRCo LeftOrRight
CRight TcCoercion
co
; evar_s <- CtLoc -> (TcType, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
loc ( CtEvidence -> TcType -> TcType -> TcType
mkTcEqPredLikeEv CtEvidence
ev TcType
s1 TcType
s2
, TcCoercion -> EvTerm
evCoercion TcCoercion
co_s )
; evar_t <- newGivenEvVar loc ( mkTcEqPredLikeEv ev t1 t2
, evCoercion co_t )
; emitWorkNC [evar_t]
; startAgainWith (mkNonCanonical evar_s) }
where
loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
s1k :: TcType
s1k = HasDebugCallStack => TcType -> TcType
TcType -> TcType
typeKind TcType
s1
s2k :: TcType
s2k = HasDebugCallStack => TcType -> TcType
TcType -> TcType
typeKind TcType
s2
TcType
k1 mismatches :: TcType -> TcType -> Bool
`mismatches` TcType
k2
= TcType -> Bool
isForAllTy TcType
k1 Bool -> Bool -> Bool
&& Bool -> Bool
not (TcType -> Bool
isForAllTy TcType
k2)
Bool -> Bool -> Bool
|| Bool -> Bool
not (TcType -> Bool
isForAllTy TcType
k1) Bool -> Bool -> Bool
&& TcType -> Bool
isForAllTy TcType
k2
canEqCast :: Bool
-> GlobalRdrEnv -> FamInstEnvs
-> CtEvidence
-> EqRel
-> SwapFlag
-> TcType -> Coercion
-> TcType -> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCast :: Bool
-> GlobalRdrEnv
-> (FamInstEnv, FamInstEnv)
-> CtEvidence
-> EqRel
-> SwapFlag
-> TcType
-> TcCoercion
-> TcType
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCast Bool
rewritten GlobalRdrEnv
rdr_env (FamInstEnv, FamInstEnv)
envs CtEvidence
ev EqRel
eq_rel SwapFlag
swapped TcType
ty1 TcCoercion
co1 TcType
ty2 TcType
ps_ty2
= do { String -> SDoc -> TcS ()
traceTcS String
"Decomposing cast" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev
, TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty1 SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"|>" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcCoercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcCoercion
co1
, TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ps_ty2 ])
; new_ev <- RewriterSet
-> CtEvidence
-> SwapFlag
-> Reduction
-> Reduction
-> TcS CtEvidence
rewriteEqEvidence RewriterSet
emptyRewriterSet CtEvidence
ev SwapFlag
swapped
(Role -> TcType -> TcCoercion -> Reduction
mkGReflLeftRedn Role
role TcType
ty1 TcCoercion
co1)
(Role -> TcType -> Reduction
mkReflRedn Role
role TcType
ps_ty2)
; can_eq_nc rewritten rdr_env envs new_ev eq_rel ty1 ty1 ty2 ps_ty2 }
where
role :: Role
role = EqRel -> Role
eqRelRole EqRel
eq_rel
canTyConApp :: CtEvidence -> EqRel
-> Bool
-> (Type,TyCon,[TcType])
-> (Type,TyCon,[TcType])
-> TcS (StopOrContinue (Either IrredCt EqCt))
canTyConApp :: CtEvidence
-> EqRel
-> Bool
-> (TcType, TyCon, [TcType])
-> (TcType, TyCon, [TcType])
-> TcS (StopOrContinue (Either IrredCt EqCt))
canTyConApp CtEvidence
ev EqRel
eq_rel Bool
both_generative (TcType
ty1,TyCon
tc1,[TcType]
tys1) (TcType
ty2,TyCon
tc2,[TcType]
tys2)
| TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
, [TcType]
tys1 [TcType] -> [TcType] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [TcType]
tys2
= do { inerts <- TcS InertSet
getInertSet
; if can_decompose inerts
then canDecomposableTyConAppOK ev eq_rel tc1 (ty1,tys1) (ty2,tys2)
else canEqSoftFailure ev eq_rel ty1 ty2 }
| TyCon -> Bool
tyConSkolem TyCon
tc1 Bool -> Bool -> Bool
|| TyCon -> Bool
tyConSkolem TyCon
tc2
= do { String -> SDoc -> TcS ()
traceTcS String
"canTyConApp: skolem abstract" (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc1 SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc2)
; CtIrredReason
-> CtEvidence -> TcS (StopOrContinue (Either IrredCt EqCt))
forall a.
CtIrredReason
-> CtEvidence -> TcS (StopOrContinue (Either IrredCt a))
finishCanWithIrred CtIrredReason
AbstractTyConReason CtEvidence
ev }
| Bool
otherwise
= if Bool
both_generative
then CtEvidence
-> TcType -> TcType -> TcS (StopOrContinue (Either IrredCt EqCt))
forall a.
CtEvidence
-> TcType -> TcType -> TcS (StopOrContinue (Either IrredCt a))
canEqHardFailure CtEvidence
ev TcType
ty1 TcType
ty2
else CtEvidence
-> EqRel
-> TcType
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
forall a.
CtEvidence
-> EqRel
-> TcType
-> TcType
-> TcS (StopOrContinue (Either IrredCt a))
canEqSoftFailure CtEvidence
ev EqRel
eq_rel TcType
ty1 TcType
ty2
where
can_decompose :: InertSet -> Bool
can_decompose InertSet
inerts
= TyCon -> Role -> Bool
isInjectiveTyCon TyCon
tc1 (EqRel -> Role
eqRelRole EqRel
eq_rel)
Bool -> Bool -> Bool
|| (Bool -> Bool -> Bool
forall a. HasCallStack => Bool -> a -> a
assert (EqRel
eq_rel EqRel -> EqRel -> Bool
forall a. Eq a => a -> a -> Bool
== EqRel
ReprEq) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev CtFlavour -> CtFlavour -> Bool
forall a. Eq a => a -> a -> Bool
== CtFlavour
Wanted Bool -> Bool -> Bool
&& TyCon -> InertSet -> Bool
noGivenNewtypeReprEqs TyCon
tc1 InertSet
inerts)
canDecomposableTyConAppOK :: CtEvidence -> EqRel
-> TyCon
-> (Type,[TcType]) -> (Type,[TcType])
-> TcS (StopOrContinue a)
canDecomposableTyConAppOK :: forall a.
CtEvidence
-> EqRel
-> TyCon
-> (TcType, [TcType])
-> (TcType, [TcType])
-> TcS (StopOrContinue a)
canDecomposableTyConAppOK CtEvidence
ev EqRel
eq_rel TyCon
tc (TcType
ty1,[TcType]
tys1) (TcType
ty2,[TcType]
tys2)
= Bool -> TcS (StopOrContinue a) -> TcS (StopOrContinue a)
forall a. HasCallStack => Bool -> a -> a
assert ([TcType]
tys1 [TcType] -> [TcType] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [TcType]
tys2) (TcS (StopOrContinue a) -> TcS (StopOrContinue a))
-> TcS (StopOrContinue a) -> TcS (StopOrContinue a)
forall a b. (a -> b) -> a -> b
$
do { String -> SDoc -> TcS ()
traceTcS String
"canDecomposableTyConAppOK"
(CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ EqRel -> SDoc
forall a. Outputable a => a -> SDoc
ppr EqRel
eq_rel SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [TcType] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcType]
tys1 SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [TcType] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcType]
tys2)
; case CtEvidence
ev of
CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest }
-> do { (co, _, _) <- CtEvidence
-> Role
-> (UnifyEnv -> TcM TcCoercion)
-> TcS (TcCoercion, Cts, [TcTyVar])
forall a.
CtEvidence
-> Role -> (UnifyEnv -> TcM a) -> TcS (a, Cts, [TcTyVar])
wrapUnifierTcS CtEvidence
ev Role
role ((UnifyEnv -> TcM TcCoercion) -> TcS (TcCoercion, Cts, [TcTyVar]))
-> (UnifyEnv -> TcM TcCoercion) -> TcS (TcCoercion, Cts, [TcTyVar])
forall a b. (a -> b) -> a -> b
$ \UnifyEnv
uenv ->
do { cos <- (CtLoc -> Role -> TcType -> TcType -> TcM TcCoercion)
-> [CtLoc]
-> [Role]
-> [TcType]
-> [TcType]
-> IOEnv (Env TcGblEnv TcLclEnv) [TcCoercion]
forall (m :: * -> *) a b c d e.
Monad m =>
(a -> b -> c -> d -> m e) -> [a] -> [b] -> [c] -> [d] -> m [e]
zipWith4M (UnifyEnv -> CtLoc -> Role -> TcType -> TcType -> TcM TcCoercion
u_arg UnifyEnv
uenv) [CtLoc]
new_locs [Role]
tc_roles [TcType]
tys1 [TcType]
tys2
; return (mkTyConAppCo role tc cos) }
; setWantedEq dest co }
CtGiven { ctev_evar :: CtEvidence -> TcTyVar
ctev_evar = TcTyVar
evar }
| let pred_ty :: TcType
pred_ty = EqRel -> TcType -> TcType -> TcType
mkEqPred EqRel
eq_rel TcType
ty1 TcType
ty2
ev_co :: TcCoercion
ev_co = TcTyVar -> TcCoercion
mkCoVarCo (TcTyVar -> TcType -> TcTyVar
setVarType TcTyVar
evar TcType
pred_ty)
-> CtLoc -> [(Role, TcCoercion)] -> TcS ()
emitNewGivens CtLoc
loc
[ (Role
r, HasDebugCallStack => CoSel -> TcCoercion -> TcCoercion
CoSel -> TcCoercion -> TcCoercion
mkSelCo (Int -> Role -> CoSel
SelTyCon Int
i Role
r) TcCoercion
ev_co)
| (Role
r, TcType
ty1, TcType
ty2, Int
i) <- [Role]
-> [TcType] -> [TcType] -> [Int] -> [(Role, TcType, TcType, Int)]
forall a b c d. [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]
zip4 [Role]
tc_roles [TcType]
tys1 [TcType]
tys2 [Int
0..]
, Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
/= Role
Phantom
, Bool -> Bool
not (TcType -> Bool
isCoercionTy TcType
ty1) Bool -> Bool -> Bool
&& Bool -> Bool
not (TcType -> Bool
isCoercionTy TcType
ty2) ]
; CtEvidence -> String -> TcS (StopOrContinue a)
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Decomposed TyConApp" }
where
loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
role :: Role
role = EqRel -> Role
eqRelRole EqRel
eq_rel
u_arg :: UnifyEnv -> CtLoc -> Role -> TcType -> TcType -> TcM TcCoercion
u_arg UnifyEnv
uenv CtLoc
arg_loc Role
arg_role = UnifyEnv -> TcType -> TcType -> TcM TcCoercion
uType UnifyEnv
arg_env
where
arg_env :: UnifyEnv
arg_env = UnifyEnv
uenv UnifyEnv -> Role -> UnifyEnv
`setUEnvRole` Role
arg_role
UnifyEnv -> (CtLoc -> CtLoc) -> UnifyEnv
`updUEnvLoc` CtLoc -> CtLoc -> CtLoc
forall a b. a -> b -> a
const CtLoc
arg_loc
tc_roles :: [Role]
tc_roles = Role -> TyCon -> [Role]
tyConRoleListX Role
role TyCon
tc
new_locs :: [CtLoc]
new_locs = [ TyConBinder -> CtLoc -> CtLoc
adjustCtLocTyConBinder TyConBinder
bndr CtLoc
loc
| TyConBinder
bndr <- TyCon -> [TyConBinder]
tyConBinders TyCon
tc ]
[CtLoc] -> [CtLoc] -> [CtLoc]
forall a. [a] -> [a] -> [a]
++ CtLoc -> [CtLoc]
forall a. a -> [a]
repeat CtLoc
loc
canDecomposableFunTy :: CtEvidence -> EqRel -> FunTyFlag
-> (Type,Type,Type,Type)
-> (Type,Type,Type,Type)
-> TcS (StopOrContinue a)
canDecomposableFunTy :: forall a.
CtEvidence
-> EqRel
-> FunTyFlag
-> (TcType, TcType, TcType, TcType)
-> (TcType, TcType, TcType, TcType)
-> TcS (StopOrContinue a)
canDecomposableFunTy CtEvidence
ev EqRel
eq_rel FunTyFlag
af f1 :: (TcType, TcType, TcType, TcType)
f1@(TcType
ty1,TcType
m1,TcType
a1,TcType
r1) f2 :: (TcType, TcType, TcType, TcType)
f2@(TcType
ty2,TcType
m2,TcType
a2,TcType
r2)
= do { String -> SDoc -> TcS ()
traceTcS String
"canDecomposableFunTy"
(CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ EqRel -> SDoc
forall a. Outputable a => a -> SDoc
ppr EqRel
eq_rel SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ (TcType, TcType, TcType, TcType) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TcType, TcType, TcType, TcType)
f1 SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ (TcType, TcType, TcType, TcType) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TcType, TcType, TcType, TcType)
f2)
; case CtEvidence
ev of
CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest }
-> do { (co, _, _) <- CtEvidence
-> Role
-> (UnifyEnv -> TcM TcCoercion)
-> TcS (TcCoercion, Cts, [TcTyVar])
forall a.
CtEvidence
-> Role -> (UnifyEnv -> TcM a) -> TcS (a, Cts, [TcTyVar])
wrapUnifierTcS CtEvidence
ev Role
Nominal ((UnifyEnv -> TcM TcCoercion) -> TcS (TcCoercion, Cts, [TcTyVar]))
-> (UnifyEnv -> TcM TcCoercion) -> TcS (TcCoercion, Cts, [TcTyVar])
forall a b. (a -> b) -> a -> b
$ \ UnifyEnv
uenv ->
do { let mult_env :: UnifyEnv
mult_env = UnifyEnv
uenv UnifyEnv -> (CtLoc -> CtLoc) -> UnifyEnv
`updUEnvLoc` CtLoc -> CtLoc
toInvisibleLoc
UnifyEnv -> Role -> UnifyEnv
`setUEnvRole` Role -> FunSel -> Role
funRole Role
role FunSel
SelMult
; mult <- UnifyEnv -> TcType -> TcType -> TcM TcCoercion
uType UnifyEnv
mult_env TcType
m1 TcType
m2
; arg <- uType (uenv `setUEnvRole` funRole role SelArg) a1 a2
; res <- uType (uenv `setUEnvRole` funRole role SelRes) r1 r2
; return (mkNakedFunCo role af mult arg res) }
; setWantedEq dest co }
CtGiven { ctev_evar :: CtEvidence -> TcTyVar
ctev_evar = TcTyVar
evar }
| let pred_ty :: TcType
pred_ty = EqRel -> TcType -> TcType -> TcType
mkEqPred EqRel
eq_rel TcType
ty1 TcType
ty2
ev_co :: TcCoercion
ev_co = TcTyVar -> TcCoercion
mkCoVarCo (TcTyVar -> TcType -> TcTyVar
setVarType TcTyVar
evar TcType
pred_ty)
-> CtLoc -> [(Role, TcCoercion)] -> TcS ()
emitNewGivens CtLoc
loc
[ (Role -> FunSel -> Role
funRole Role
role FunSel
fs, HasDebugCallStack => CoSel -> TcCoercion -> TcCoercion
CoSel -> TcCoercion -> TcCoercion
mkSelCo (FunSel -> CoSel
SelFun FunSel
fs) TcCoercion
ev_co)
| FunSel
fs <- [FunSel
SelMult, FunSel
SelArg, FunSel
SelRes] ]
; CtEvidence -> String -> TcS (StopOrContinue a)
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Decomposed TyConApp" }
where
loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
role :: Role
role = EqRel -> Role
eqRelRole EqRel
eq_rel
canEqSoftFailure :: CtEvidence -> EqRel -> TcType -> TcType
-> TcS (StopOrContinue (Either IrredCt a))
canEqSoftFailure :: forall a.
CtEvidence
-> EqRel
-> TcType
-> TcType
-> TcS (StopOrContinue (Either IrredCt a))
canEqSoftFailure CtEvidence
ev EqRel
NomEq TcType
ty1 TcType
ty2
= CtEvidence
-> TcType -> TcType -> TcS (StopOrContinue (Either IrredCt a))
forall a.
CtEvidence
-> TcType -> TcType -> TcS (StopOrContinue (Either IrredCt a))
canEqHardFailure CtEvidence
ev TcType
ty1 TcType
ty2
canEqSoftFailure CtEvidence
ev EqRel
ReprEq TcType
ty1 TcType
ty2
= do { (redn1, rewriters1) <- CtEvidence -> TcType -> TcS (Reduction, RewriterSet)
rewrite CtEvidence
ev TcType
ty1
; (redn2, rewriters2) <- rewrite ev ty2
; traceTcS "canEqSoftFailure with ReprEq" $
vcat [ ppr ev, ppr redn1, ppr redn2 ]
; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped redn1 redn2
; finishCanWithIrred ReprEqReason new_ev }
canEqHardFailure :: CtEvidence -> TcType -> TcType
-> TcS (StopOrContinue (Either IrredCt a))
canEqHardFailure :: forall a.
CtEvidence
-> TcType -> TcType -> TcS (StopOrContinue (Either IrredCt a))
canEqHardFailure CtEvidence
ev TcType
ty1 TcType
ty2
= do { String -> SDoc -> TcS ()
traceTcS String
"canEqHardFailure" (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty1 SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty2)
; (redn1, rewriters1) <- CtEvidence -> TcType -> TcS (Reduction, RewriterSet)
rewriteForErrors CtEvidence
ev TcType
ty1
; (redn2, rewriters2) <- rewriteForErrors ev ty2
; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped redn1 redn2
; finishCanWithIrred ShapeMismatchReason new_ev }
canEqCanLHS :: CtEvidence
-> EqRel -> SwapFlag
-> CanEqLHS
-> TcType
-> TcType -> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCanLHS :: CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> TcType
-> TcType
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCanLHS CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 TcType
ps_xi1 TcType
xi2 TcType
ps_xi2
| TcType
k1 HasDebugCallStack => TcType -> TcType -> Bool
TcType -> TcType -> Bool
`tcEqType` TcType
k2
= CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> TcType
-> TcType
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCanLHSHomo CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 TcType
ps_xi1 TcType
xi2 TcType
ps_xi2
| Bool
otherwise
= CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> TcType
-> TcType
-> TcType
-> TcType
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCanLHSHetero CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 TcType
ps_xi1 TcType
k1 TcType
xi2 TcType
ps_xi2 TcType
k2
where
k1 :: TcType
k1 = CanEqLHS -> TcType
canEqLHSKind CanEqLHS
lhs1
k2 :: TcType
k2 = HasDebugCallStack => TcType -> TcType
TcType -> TcType
typeKind TcType
xi2
canEqCanLHSHetero :: CtEvidence
-> EqRel -> SwapFlag
-> CanEqLHS -> TcType
-> TcKind
-> TcType -> TcType
-> TcKind
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCanLHSHetero :: CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> TcType
-> TcType
-> TcType
-> TcType
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCanLHSHetero CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 TcType
ps_xi1 TcType
ki1 TcType
xi2 TcType
ps_xi2 TcType
ki2
= do { (kind_co, rewriters, unifs_happened) <- TcS (TcCoercion, RewriterSet, Bool)
mk_kind_eq
; if unifs_happened
then startAgainWith (mkNonCanonical ev)
else
do { let lhs_redn = Role -> TcType -> Reduction
mkReflRedn Role
role TcType
ps_xi1
rhs_redn = Role -> TcType -> TcCoercion -> Reduction
mkGReflRightRedn Role
role TcType
xi2 TcCoercion
mb_sym_kind_co
mb_sym_kind_co = case SwapFlag
swapped of
SwapFlag
NotSwapped -> TcCoercion -> TcCoercion
mkSymCo TcCoercion
kind_co
SwapFlag
IsSwapped -> TcCoercion
kind_co
; traceTcS "Hetero equality gives rise to kind equality"
(ppr swapped $$
ppr kind_co <+> dcolon <+> sep [ ppr ki1, text "~#", ppr ki2 ])
; type_ev <- rewriteEqEvidence rewriters ev swapped lhs_redn rhs_redn
; let new_xi2 = TcType -> TcCoercion -> TcType
mkCastTy TcType
ps_xi2 TcCoercion
mb_sym_kind_co
; canEqCanLHSHomo type_ev eq_rel NotSwapped lhs1 ps_xi1 new_xi2 new_xi2 }}
where
mk_kind_eq :: TcS (CoercionN, RewriterSet, Bool)
mk_kind_eq :: TcS (TcCoercion, RewriterSet, Bool)
mk_kind_eq = case CtEvidence
ev of
CtGiven { ctev_evar :: CtEvidence -> TcTyVar
ctev_evar = TcTyVar
evar }
-> do { let kind_co :: TcCoercion
kind_co = TcCoercion -> TcCoercion
mkKindCo (TcTyVar -> TcCoercion
mkCoVarCo TcTyVar
evar)
pred_ty :: TcType
pred_ty = SwapFlag
-> (TcType -> TcType -> TcType) -> TcType -> TcType -> TcType
forall a b. SwapFlag -> (a -> a -> b) -> a -> a -> b
unSwap SwapFlag
swapped TcType -> TcType -> TcType
mkNomEqPred TcType
ki1 TcType
ki2
kind_loc :: CtLoc
kind_loc = TcType -> TcType -> CtLoc -> CtLoc
mkKindEqLoc TcType
xi1 TcType
xi2 (CtEvidence -> CtLoc
ctev_loc CtEvidence
ev)
; kind_ev <- CtLoc -> (TcType, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
kind_loc (TcType
pred_ty, TcCoercion -> EvTerm
evCoercion TcCoercion
kind_co)
; emitWorkNC [kind_ev]
; return (ctEvCoercion kind_ev, emptyRewriterSet, False) }
CtWanted {}
-> do { (kind_co, cts, unifs) <- CtEvidence
-> Role
-> (UnifyEnv -> TcM TcCoercion)
-> TcS (TcCoercion, Cts, [TcTyVar])
forall a.
CtEvidence
-> Role -> (UnifyEnv -> TcM a) -> TcS (a, Cts, [TcTyVar])
wrapUnifierTcS CtEvidence
ev Role
Nominal ((UnifyEnv -> TcM TcCoercion) -> TcS (TcCoercion, Cts, [TcTyVar]))
-> (UnifyEnv -> TcM TcCoercion) -> TcS (TcCoercion, Cts, [TcTyVar])
forall a b. (a -> b) -> a -> b
$ \UnifyEnv
uenv ->
let uenv' :: UnifyEnv
uenv' = UnifyEnv -> (CtLoc -> CtLoc) -> UnifyEnv
updUEnvLoc UnifyEnv
uenv (TcType -> TcType -> CtLoc -> CtLoc
mkKindEqLoc TcType
xi1 TcType
xi2)
in SwapFlag
-> (TcType -> TcType -> TcM TcCoercion)
-> TcType
-> TcType
-> TcM TcCoercion
forall a b. SwapFlag -> (a -> a -> b) -> a -> a -> b
unSwap SwapFlag
swapped (UnifyEnv -> TcType -> TcType -> TcM TcCoercion
uType UnifyEnv
uenv') TcType
ki1 TcType
ki2
; return (kind_co, rewriterSetFromCts cts, not (null unifs)) }
xi1 :: TcType
xi1 = CanEqLHS -> TcType
canEqLHSType CanEqLHS
lhs1
role :: Role
role = EqRel -> Role
eqRelRole EqRel
eq_rel
canEqCanLHSHomo :: CtEvidence
-> EqRel -> SwapFlag
-> CanEqLHS -> TcType
-> TcType -> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCanLHSHomo :: CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> TcType
-> TcType
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCanLHSHomo CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 TcType
ps_xi1 TcType
xi2 TcType
ps_xi2
| (TcType
xi2', MCoercion
mco) <- TcType -> (TcType, MCoercion)
split_cast_ty TcType
xi2
, Just CanEqLHS
lhs2 <- TcType -> Maybe CanEqLHS
canEqLHS_maybe TcType
xi2'
= CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> TcType
-> CanEqLHS
-> TcType
-> MCoercion
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCanLHS2 CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 TcType
ps_xi1 CanEqLHS
lhs2 (TcType
ps_xi2 TcType -> MCoercion -> TcType
`mkCastTyMCo` MCoercion -> MCoercion
mkSymMCo MCoercion
mco) MCoercion
mco
| Bool
otherwise
= CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCanLHSFinish CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 TcType
ps_xi2
where
split_cast_ty :: TcType -> (TcType, MCoercion)
split_cast_ty (CastTy TcType
ty TcCoercion
co) = (TcType
ty, TcCoercion -> MCoercion
MCo TcCoercion
co)
split_cast_ty TcType
other = (TcType
other, MCoercion
MRefl)
canEqCanLHS2 :: CtEvidence
-> EqRel -> SwapFlag
-> CanEqLHS
-> TcType
-> CanEqLHS
-> TcType
-> MCoercion
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCanLHS2 :: CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> TcType
-> CanEqLHS
-> TcType
-> MCoercion
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCanLHS2 CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 TcType
ps_xi1 CanEqLHS
lhs2 TcType
ps_xi2 MCoercion
mco
| CanEqLHS
lhs1 CanEqLHS -> CanEqLHS -> Bool
`eqCanEqLHS` CanEqLHS
lhs2
= CtEvidence
-> EqRel -> TcType -> TcS (StopOrContinue (Either IrredCt EqCt))
forall a. CtEvidence -> EqRel -> TcType -> TcS (StopOrContinue a)
canEqReflexive CtEvidence
ev EqRel
eq_rel TcType
lhs1_ty
| TyVarLHS TcTyVar
tv1 <- CanEqLHS
lhs1
, TyVarLHS TcTyVar
tv2 <- CanEqLHS
lhs2
=
do { String -> SDoc -> TcS ()
traceTcS String
"canEqLHS2 swapOver" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv1 SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv2 SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ SwapFlag -> SDoc
forall a. Outputable a => a -> SDoc
ppr SwapFlag
swapped)
; if Bool -> TcTyVar -> TcTyVar -> Bool
swapOverTyVars (CtEvidence -> Bool
isGiven CtEvidence
ev) TcTyVar
tv1 TcTyVar
tv2
then TcS (StopOrContinue (Either IrredCt EqCt))
finish_with_swapping
else TcS (StopOrContinue (Either IrredCt EqCt))
finish_without_swapping }
| TyVarLHS {} <- CanEqLHS
lhs1
, TyFamLHS {} <- CanEqLHS
lhs2
= if Bool
put_tyvar_on_lhs
then TcS (StopOrContinue (Either IrredCt EqCt))
finish_without_swapping
else TcS (StopOrContinue (Either IrredCt EqCt))
finish_with_swapping
| TyFamLHS {} <- CanEqLHS
lhs1
, TyVarLHS {} <- CanEqLHS
lhs2
= if Bool
put_tyvar_on_lhs
then TcS (StopOrContinue (Either IrredCt EqCt))
finish_with_swapping
else TcS (StopOrContinue (Either IrredCt EqCt))
finish_without_swapping
| TyFamLHS TyCon
_fun_tc1 [TcType]
fun_args1 <- CanEqLHS
lhs1
, TyFamLHS TyCon
_fun_tc2 [TcType]
fun_args2 <- CanEqLHS
lhs2
= do { String -> SDoc -> TcS ()
traceTcS String
"canEqCanLHS2 two type families" (CanEqLHS -> SDoc
forall a. Outputable a => a -> SDoc
ppr CanEqLHS
lhs1 SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ CanEqLHS -> SDoc
forall a. Outputable a => a -> SDoc
ppr CanEqLHS
lhs2)
; tclvl <- TcS TcLevel
getTcLevel
; let tvs1 = [TcType] -> TyCoVarSet
tyCoVarsOfTypes [TcType]
fun_args1
tvs2 = [TcType] -> TyCoVarSet
tyCoVarsOfTypes [TcType]
fun_args2
swap_for_size = [TcType] -> Int
typesSize [TcType]
fun_args2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> [TcType] -> Int
typesSize [TcType]
fun_args1
meta_tv_lhs = (TcTyVar -> Bool) -> TyCoVarSet -> Bool
anyVarSet (TcLevel -> TcTyVar -> Bool
isTouchableMetaTyVar TcLevel
tclvl) TyCoVarSet
tvs1
meta_tv_rhs = (TcTyVar -> Bool) -> TyCoVarSet -> Bool
anyVarSet (TcLevel -> TcTyVar -> Bool
isTouchableMetaTyVar TcLevel
tclvl) TyCoVarSet
tvs2
swap_for_rewriting = Bool
meta_tv_rhs Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
meta_tv_lhs
; if swap_for_rewriting || (meta_tv_lhs == meta_tv_rhs && swap_for_size)
then finish_with_swapping
else finish_without_swapping }
where
sym_mco :: MCoercion
sym_mco = MCoercion -> MCoercion
mkSymMCo MCoercion
mco
role :: Role
role = EqRel -> Role
eqRelRole EqRel
eq_rel
lhs1_ty :: TcType
lhs1_ty = CanEqLHS -> TcType
canEqLHSType CanEqLHS
lhs1
lhs2_ty :: TcType
lhs2_ty = CanEqLHS -> TcType
canEqLHSType CanEqLHS
lhs2
finish_without_swapping :: TcS (StopOrContinue (Either IrredCt EqCt))
finish_without_swapping
= CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCanLHSFinish CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs1 (TcType
ps_xi2 TcType -> MCoercion -> TcType
`mkCastTyMCo` MCoercion
mco)
finish_with_swapping :: TcS (StopOrContinue (Either IrredCt EqCt))
finish_with_swapping
= do { let lhs1_redn :: Reduction
lhs1_redn = Role -> TcType -> MCoercion -> Reduction
mkGReflRightMRedn Role
role TcType
lhs1_ty MCoercion
sym_mco
lhs2_redn :: Reduction
lhs2_redn = Role -> TcType -> MCoercion -> Reduction
mkGReflLeftMRedn Role
role TcType
lhs2_ty MCoercion
mco
; new_ev <-RewriterSet
-> CtEvidence
-> SwapFlag
-> Reduction
-> Reduction
-> TcS CtEvidence
rewriteEqEvidence RewriterSet
emptyRewriterSet CtEvidence
ev SwapFlag
swapped Reduction
lhs1_redn Reduction
lhs2_redn
; canEqCanLHSFinish new_ev eq_rel IsSwapped lhs2 (ps_xi1 `mkCastTyMCo` sym_mco) }
put_tyvar_on_lhs :: Bool
put_tyvar_on_lhs = CtEvidence -> Bool
isWanted CtEvidence
ev Bool -> Bool -> Bool
&& EqRel
eq_rel EqRel -> EqRel -> Bool
forall a. Eq a => a -> a -> Bool
== EqRel
NomEq
canEqCanLHSFinish, canEqCanLHSFinish_try_unification,
canEqCanLHSFinish_no_unification
:: CtEvidence
-> EqRel -> SwapFlag
-> CanEqLHS
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCanLHSFinish :: CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCanLHSFinish CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs TcType
rhs
= do { String -> SDoc -> TcS ()
traceTcS String
"canEqCanLHSFinish" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ev:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"swapped:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SwapFlag -> SDoc
forall a. Outputable a => a -> SDoc
ppr SwapFlag
swapped
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"lhs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CanEqLHS -> SDoc
forall a. Outputable a => a -> SDoc
ppr CanEqLHS
lhs
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"rhs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
rhs ]
; Bool -> TcS ()
forall (m :: * -> *). (HasCallStack, Applicative m) => Bool -> m ()
massert (CanEqLHS -> TcType
canEqLHSKind CanEqLHS
lhs HasCallStack => TcType -> TcType -> Bool
TcType -> TcType -> Bool
`eqType` HasDebugCallStack => TcType -> TcType
TcType -> TcType
typeKind TcType
rhs)
; TcS Bool -> SDoc -> TcS ()
forall (m :: * -> *).
(HasCallStack, Monad m) =>
m Bool -> SDoc -> m ()
assertPprM TcS Bool
ty_eq_N_OK (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"CanEqCanLHSFinish: (TyEq:N) not satisfied"
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"rhs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
rhs ]
; CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCanLHSFinish_try_unification CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs TcType
rhs }
where
ty_eq_N_OK :: TcS Bool
ty_eq_N_OK :: TcS Bool
ty_eq_N_OK
| EqRel
ReprEq <- EqRel
eq_rel
, Just (TyCon
tc, [TcType]
tc_args) <- HasDebugCallStack => TcType -> Maybe (TyCon, [TcType])
TcType -> Maybe (TyCon, [TcType])
splitTyConApp_maybe TcType
rhs
, Just DataCon
con <- TyCon -> Maybe DataCon
newTyConDataCon_maybe TyCon
tc
, [TcType]
tc_args [TcType] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthAtLeast` TyCon -> Int
tyConArity TyCon
tc
= do { rdr_env <- TcS GlobalRdrEnv
getGlobalRdrEnvTcS
; let con_in_scope = Maybe GlobalRdrElt -> Bool
forall a. Maybe a -> Bool
isJust (Maybe GlobalRdrElt -> Bool) -> Maybe GlobalRdrElt -> Bool
forall a b. (a -> b) -> a -> b
$ GlobalRdrEnv -> Name -> Maybe GlobalRdrElt
forall info.
Outputable info =>
GlobalRdrEnvX info -> Name -> Maybe (GlobalRdrEltX info)
lookupGRE_Name GlobalRdrEnv
rdr_env (DataCon -> Name
dataConName DataCon
con)
; return $ not con_in_scope }
| Bool
otherwise
= Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
canEqCanLHSFinish_try_unification :: CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCanLHSFinish_try_unification CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs TcType
rhs
| CtEvidence -> Bool
isWanted CtEvidence
ev
, EqRel
NomEq <- EqRel
eq_rel
, TyVarLHS TcTyVar
tv <- CanEqLHS
lhs
= do { given_eq_lvl <- TcS TcLevel
getInnermostGivenEqLevel
; if not (touchabilityAndShapeTest given_eq_lvl tv rhs)
then if | Just can_rhs <- canTyFamEqLHS_maybe rhs
-> swapAndFinish ev eq_rel swapped (mkTyVarTy tv) can_rhs
| otherwise
-> canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
else
do { check_result <- checkTouchableTyVarEq ev tv rhs
; case check_result of {
PuFail CheckTyEqResult
reason
| Just CanEqLHS
can_rhs <- TcType -> Maybe CanEqLHS
canTyFamEqLHS_maybe TcType
rhs
-> CtEvidence
-> EqRel
-> SwapFlag
-> TcType
-> CanEqLHS
-> TcS (StopOrContinue (Either IrredCt EqCt))
forall unused.
CtEvidence
-> EqRel
-> SwapFlag
-> TcType
-> CanEqLHS
-> TcS (StopOrContinue (Either unused EqCt))
swapAndFinish CtEvidence
ev EqRel
eq_rel SwapFlag
swapped (TcTyVar -> TcType
mkTyVarTy TcTyVar
tv) CanEqLHS
can_rhs
| CheckTyEqResult
reason CheckTyEqResult -> CheckTyEqResult -> Bool
`cterHasOnlyProblems` CheckTyEqResult
do_not_prevent_rewriting
-> CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCanLHSFinish_no_unification CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs TcType
rhs
| Bool
otherwise
-> CheckTyEqResult
-> CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
forall unused.
CheckTyEqResult
-> CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> TcType
-> TcS (StopOrContinue (Either IrredCt unused))
tryIrredInstead CheckTyEqResult
reason CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs TcType
rhs ;
PuOK Bag ()
_ Reduction
rhs_redn ->
do {
new_ev <- if TcCoercion -> Bool
isReflCo (Reduction -> TcCoercion
reductionCoercion Reduction
rhs_redn)
then CtEvidence -> TcS CtEvidence
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return CtEvidence
ev
else RewriterSet
-> CtEvidence
-> SwapFlag
-> Reduction
-> Reduction
-> TcS CtEvidence
rewriteEqEvidence RewriterSet
emptyRewriterSet CtEvidence
ev SwapFlag
swapped
(Role -> TcType -> Reduction
mkReflRedn Role
Nominal (TcTyVar -> TcType
mkTyVarTy TcTyVar
tv)) Reduction
rhs_redn
; let tv_ty = TcTyVar -> TcType
mkTyVarTy TcTyVar
tv
final_rhs = Reduction -> TcType
reductionReducedType Reduction
rhs_redn
; traceTcS "Sneaky unification:" $
vcat [text "Unifies:" <+> ppr tv <+> text ":=" <+> ppr final_rhs,
text "Coercion:" <+> pprEq tv_ty final_rhs,
text "Left Kind is:" <+> ppr (typeKind tv_ty),
text "Right Kind is:" <+> ppr (typeKind final_rhs) ]
; unifyTyVar tv final_rhs
; setEvBindIfWanted new_ev EvCanonical $
evCoercion (mkNomReflCo final_rhs)
; kickOutAfterUnification [tv]
; return (Stop new_ev (text "Solved by unification")) }}}}
| Bool
otherwise
= CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCanLHSFinish_no_unification CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs TcType
rhs
where
do_not_prevent_rewriting :: CheckTyEqResult
do_not_prevent_rewriting :: CheckTyEqResult
do_not_prevent_rewriting = CheckTyEqProblem -> CheckTyEqResult
cteProblem CheckTyEqProblem
cteSkolemEscape CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult
forall a. Semigroup a => a -> a -> a
S.<>
CheckTyEqProblem -> CheckTyEqResult
cteProblem CheckTyEqProblem
cteConcrete
canEqCanLHSFinish_no_unification :: CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCanLHSFinish_no_unification CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs TcType
rhs
= do {
; check_result <- CtEvidence
-> EqRel -> CanEqLHS -> TcType -> TcS (PuResult () Reduction)
checkTypeEq CtEvidence
ev EqRel
eq_rel CanEqLHS
lhs TcType
rhs
; let lhs_ty = CanEqLHS -> TcType
canEqLHSType CanEqLHS
lhs
; case check_result of
PuFail CheckTyEqResult
reason
-> CheckTyEqResult
-> CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> TcType
-> TcS (StopOrContinue (Either IrredCt EqCt))
forall unused.
CheckTyEqResult
-> CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> TcType
-> TcS (StopOrContinue (Either IrredCt unused))
tryIrredInstead CheckTyEqResult
reason CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs TcType
rhs
PuOK Bag ()
_ Reduction
rhs_redn
-> do { new_ev <- RewriterSet
-> CtEvidence
-> SwapFlag
-> Reduction
-> Reduction
-> TcS CtEvidence
rewriteEqEvidence RewriterSet
emptyRewriterSet CtEvidence
ev SwapFlag
swapped
(Role -> TcType -> Reduction
mkReflRedn (EqRel -> Role
eqRelRole EqRel
eq_rel) TcType
lhs_ty)
Reduction
rhs_redn
; continueWith $ Right $
EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel
, eq_lhs = lhs
, eq_rhs = reductionReducedType rhs_redn } } }
swapAndFinish :: CtEvidence -> EqRel -> SwapFlag
-> TcType -> CanEqLHS
-> TcS (StopOrContinue (Either unused EqCt))
swapAndFinish :: forall unused.
CtEvidence
-> EqRel
-> SwapFlag
-> TcType
-> CanEqLHS
-> TcS (StopOrContinue (Either unused EqCt))
swapAndFinish CtEvidence
ev EqRel
eq_rel SwapFlag
swapped TcType
lhs_ty CanEqLHS
can_rhs
= do { let role :: Role
role = EqRel -> Role
eqRelRole EqRel
eq_rel
; new_ev <- RewriterSet
-> CtEvidence
-> SwapFlag
-> Reduction
-> Reduction
-> TcS CtEvidence
rewriteEqEvidence RewriterSet
emptyRewriterSet CtEvidence
ev (SwapFlag -> SwapFlag
flipSwap SwapFlag
swapped)
(Role -> TcType -> Reduction
mkReflRedn Role
role (CanEqLHS -> TcType
canEqLHSType CanEqLHS
can_rhs))
(Role -> TcType -> Reduction
mkReflRedn Role
role TcType
lhs_ty)
; continueWith $ Right $
EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel
, eq_lhs = can_rhs, eq_rhs = lhs_ty } }
tryIrredInstead :: CheckTyEqResult -> CtEvidence
-> EqRel -> SwapFlag -> CanEqLHS -> TcType
-> TcS (StopOrContinue (Either IrredCt unused))
tryIrredInstead :: forall unused.
CheckTyEqResult
-> CtEvidence
-> EqRel
-> SwapFlag
-> CanEqLHS
-> TcType
-> TcS (StopOrContinue (Either IrredCt unused))
tryIrredInstead CheckTyEqResult
reason CtEvidence
ev EqRel
eq_rel SwapFlag
swapped CanEqLHS
lhs TcType
rhs
= do { String -> SDoc -> TcS ()
traceTcS String
"cantMakeCanonical" (CheckTyEqResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr CheckTyEqResult
reason SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ CanEqLHS -> SDoc
forall a. Outputable a => a -> SDoc
ppr CanEqLHS
lhs SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
rhs)
; let role :: Role
role = EqRel -> Role
eqRelRole EqRel
eq_rel
; new_ev <- RewriterSet
-> CtEvidence
-> SwapFlag
-> Reduction
-> Reduction
-> TcS CtEvidence
rewriteEqEvidence RewriterSet
emptyRewriterSet CtEvidence
ev SwapFlag
swapped
(Role -> TcType -> Reduction
mkReflRedn Role
role (CanEqLHS -> TcType
canEqLHSType CanEqLHS
lhs))
(Role -> TcType -> Reduction
mkReflRedn Role
role TcType
rhs)
; finishCanWithIrred (NonCanonicalReason reason) new_ev }
finishCanWithIrred :: CtIrredReason -> CtEvidence
-> TcS (StopOrContinue (Either IrredCt a))
finishCanWithIrred :: forall a.
CtIrredReason
-> CtEvidence -> TcS (StopOrContinue (Either IrredCt a))
finishCanWithIrred CtIrredReason
reason CtEvidence
ev
= do {
Bool -> TcS () -> TcS ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (CtIrredReason -> Bool
isInsolubleReason CtIrredReason
reason) TcS ()
tryEarlyAbortTcS
; Either IrredCt a -> TcS (StopOrContinue (Either IrredCt a))
forall a. a -> TcS (StopOrContinue a)
continueWith (Either IrredCt a -> TcS (StopOrContinue (Either IrredCt a)))
-> Either IrredCt a -> TcS (StopOrContinue (Either IrredCt a))
forall a b. (a -> b) -> a -> b
$ IrredCt -> Either IrredCt a
forall a b. a -> Either a b
Left (IrredCt -> Either IrredCt a) -> IrredCt -> Either IrredCt a
forall a b. (a -> b) -> a -> b
$ IrredCt { ir_ev :: CtEvidence
ir_ev = CtEvidence
ev, ir_reason :: CtIrredReason
ir_reason = CtIrredReason
reason } }
canEqReflexive :: CtEvidence
-> EqRel
-> TcType
-> TcS (StopOrContinue a)
canEqReflexive :: forall a. CtEvidence -> EqRel -> TcType -> TcS (StopOrContinue a)
canEqReflexive CtEvidence
ev EqRel
eq_rel TcType
ty
= do { CtEvidence -> CanonicalEvidence -> EvTerm -> TcS ()
setEvBindIfWanted CtEvidence
ev CanonicalEvidence
EvCanonical (EvTerm -> TcS ()) -> EvTerm -> TcS ()
forall a b. (a -> b) -> a -> b
$
TcCoercion -> EvTerm
evCoercion (Role -> TcType -> TcCoercion
mkReflCo (EqRel -> Role
eqRelRole EqRel
eq_rel) TcType
ty)
; CtEvidence -> String -> TcS (StopOrContinue a)
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Solved by reflexivity" }
rewriteEqEvidence :: RewriterSet
-> CtEvidence
-> SwapFlag
-> Reduction
-> Reduction
-> TcS CtEvidence
rewriteEqEvidence :: RewriterSet
-> CtEvidence
-> SwapFlag
-> Reduction
-> Reduction
-> TcS CtEvidence
rewriteEqEvidence RewriterSet
new_rewriters CtEvidence
old_ev SwapFlag
swapped (Reduction TcCoercion
lhs_co TcType
nlhs) (Reduction TcCoercion
rhs_co TcType
nrhs)
| SwapFlag
NotSwapped <- SwapFlag
swapped
, TcCoercion -> Bool
isReflCo TcCoercion
lhs_co
, TcCoercion -> Bool
isReflCo TcCoercion
rhs_co
= CtEvidence -> TcS CtEvidence
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (HasDebugCallStack => CtEvidence -> TcType -> CtEvidence
CtEvidence -> TcType -> CtEvidence
setCtEvPredType CtEvidence
old_ev TcType
new_pred)
| CtGiven { ctev_evar :: CtEvidence -> TcTyVar
ctev_evar = TcTyVar
old_evar } <- CtEvidence
old_ev
= do { let new_tm :: EvTerm
new_tm = TcCoercion -> EvTerm
evCoercion ( TcCoercion -> TcCoercion
mkSymCo TcCoercion
lhs_co
HasDebugCallStack => TcCoercion -> TcCoercion -> TcCoercion
TcCoercion -> TcCoercion -> TcCoercion
`mkTransCo` SwapFlag -> TcCoercion -> TcCoercion
maybeSymCo SwapFlag
swapped (TcTyVar -> TcCoercion
mkCoVarCo TcTyVar
old_evar)
HasDebugCallStack => TcCoercion -> TcCoercion -> TcCoercion
TcCoercion -> TcCoercion -> TcCoercion
`mkTransCo` TcCoercion
rhs_co)
; CtLoc -> (TcType, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
loc (TcType
new_pred, EvTerm
new_tm) }
| CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest
, ctev_rewriters :: CtEvidence -> RewriterSet
ctev_rewriters = RewriterSet
rewriters } <- CtEvidence
old_ev
, let rewriters' :: RewriterSet
rewriters' = RewriterSet
rewriters RewriterSet -> RewriterSet -> RewriterSet
forall a. Semigroup a => a -> a -> a
S.<> RewriterSet
new_rewriters
= do { (new_ev, hole_co) <- CtLoc
-> RewriterSet
-> Role
-> TcType
-> TcType
-> TcS (CtEvidence, TcCoercion)
newWantedEq CtLoc
loc RewriterSet
rewriters' (HasDebugCallStack => CtEvidence -> Role
CtEvidence -> Role
ctEvRewriteRole CtEvidence
old_ev) TcType
nlhs TcType
nrhs
; let co = SwapFlag -> TcCoercion -> TcCoercion
maybeSymCo SwapFlag
swapped (TcCoercion -> TcCoercion) -> TcCoercion -> TcCoercion
forall a b. (a -> b) -> a -> b
$
TcCoercion
lhs_co HasDebugCallStack => TcCoercion -> TcCoercion -> TcCoercion
TcCoercion -> TcCoercion -> TcCoercion
`mkTransCo` TcCoercion
hole_co HasDebugCallStack => TcCoercion -> TcCoercion -> TcCoercion
TcCoercion -> TcCoercion -> TcCoercion
`mkTransCo` TcCoercion -> TcCoercion
mkSymCo TcCoercion
rhs_co
; setWantedEq dest co
; traceTcS "rewriteEqEvidence" (vcat [ ppr old_ev
, ppr nlhs
, ppr nrhs
, ppr co
, ppr new_rewriters ])
; return new_ev }
where
new_pred :: TcType
new_pred = CtEvidence -> TcType -> TcType -> TcType
mkTcEqPredLikeEv CtEvidence
old_ev TcType
nlhs TcType
nrhs
loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
old_ev
tryInertEqs :: EqCt -> SolverStage ()
tryInertEqs :: EqCt -> SolverStage ()
tryInertEqs work_item :: EqCt
work_item@(EqCt { eq_ev :: EqCt -> CtEvidence
eq_ev = CtEvidence
ev, eq_eq_rel :: EqCt -> EqRel
eq_eq_rel = EqRel
eq_rel })
= TcS (StopOrContinue ()) -> SolverStage ()
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue ()) -> SolverStage ())
-> TcS (StopOrContinue ()) -> SolverStage ()
forall a b. (a -> b) -> a -> b
$
do { inerts <- TcS InertCans
getInertCans
; if | Just (ev_i, swapped) <- inertsCanDischarge inerts work_item
-> do { setEvBindIfWanted ev EvCanonical $
evCoercion (maybeSymCo swapped $
downgradeRole (eqRelRole eq_rel)
(ctEvRewriteRole ev_i)
(ctEvCoercion ev_i))
; stopWith ev "Solved from inert" }
| otherwise
-> continueWith () }
inertsCanDischarge :: InertCans -> EqCt
-> Maybe ( CtEvidence
, SwapFlag )
inertsCanDischarge :: InertCans -> EqCt -> Maybe (CtEvidence, SwapFlag)
inertsCanDischarge InertCans
inerts (EqCt { eq_lhs :: EqCt -> CanEqLHS
eq_lhs = CanEqLHS
lhs_w, eq_rhs :: EqCt -> TcType
eq_rhs = TcType
rhs_w
, eq_ev :: EqCt -> CtEvidence
eq_ev = CtEvidence
ev_w, eq_eq_rel :: EqCt -> EqRel
eq_eq_rel = EqRel
eq_rel })
| (CtEvidence
ev_i : [CtEvidence]
_) <- [ CtEvidence
ev_i | EqCt { eq_ev :: EqCt -> CtEvidence
eq_ev = CtEvidence
ev_i, eq_rhs :: EqCt -> TcType
eq_rhs = TcType
rhs_i
, eq_eq_rel :: EqCt -> EqRel
eq_eq_rel = EqRel
eq_rel }
<- InertCans -> CanEqLHS -> [EqCt]
findEq InertCans
inerts CanEqLHS
lhs_w
, TcType
rhs_i HasDebugCallStack => TcType -> TcType -> Bool
TcType -> TcType -> Bool
`tcEqType` TcType
rhs_w
, CtEvidence -> EqRel -> Bool
inert_beats_wanted CtEvidence
ev_i EqRel
eq_rel ]
=
(CtEvidence, SwapFlag) -> Maybe (CtEvidence, SwapFlag)
forall a. a -> Maybe a
Just (CtEvidence
ev_i, SwapFlag
NotSwapped)
| Just CanEqLHS
rhs_lhs <- TcType -> Maybe CanEqLHS
canEqLHS_maybe TcType
rhs_w
, (CtEvidence
ev_i : [CtEvidence]
_) <- [ CtEvidence
ev_i | EqCt { eq_ev :: EqCt -> CtEvidence
eq_ev = CtEvidence
ev_i, eq_rhs :: EqCt -> TcType
eq_rhs = TcType
rhs_i
, eq_eq_rel :: EqCt -> EqRel
eq_eq_rel = EqRel
eq_rel }
<- InertCans -> CanEqLHS -> [EqCt]
findEq InertCans
inerts CanEqLHS
rhs_lhs
, TcType
rhs_i HasDebugCallStack => TcType -> TcType -> Bool
TcType -> TcType -> Bool
`tcEqType` CanEqLHS -> TcType
canEqLHSType CanEqLHS
lhs_w
, CtEvidence -> EqRel -> Bool
inert_beats_wanted CtEvidence
ev_i EqRel
eq_rel ]
=
(CtEvidence, SwapFlag) -> Maybe (CtEvidence, SwapFlag)
forall a. a -> Maybe a
Just (CtEvidence
ev_i, SwapFlag
IsSwapped)
where
loc_w :: CtLoc
loc_w = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev_w
flav_w :: CtFlavour
flav_w = CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev_w
fr_w :: CtFlavourRole
fr_w = (CtFlavour
flav_w, EqRel
eq_rel)
inert_beats_wanted :: CtEvidence -> EqRel -> Bool
inert_beats_wanted CtEvidence
ev_i EqRel
eq_rel
=
CtFlavourRole
fr_i CtFlavourRole -> CtFlavourRole -> Bool
`eqCanRewriteFR` CtFlavourRole
fr_w
Bool -> Bool -> Bool
&& Bool -> Bool
not ((CtLoc
loc_w CtLoc -> CtLoc -> Bool
`strictly_more_visible` CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev_i)
Bool -> Bool -> Bool
&& (CtFlavourRole
fr_w CtFlavourRole -> CtFlavourRole -> Bool
`eqCanRewriteFR` CtFlavourRole
fr_i))
where
fr_i :: CtFlavourRole
fr_i = (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev_i, EqRel
eq_rel)
strictly_more_visible :: CtLoc -> CtLoc -> Bool
strictly_more_visible CtLoc
loc1 CtLoc
loc2
= Bool -> Bool
not (CtOrigin -> Bool
isVisibleOrigin (CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc2)) Bool -> Bool -> Bool
&&
CtOrigin -> Bool
isVisibleOrigin (CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc1)
inertsCanDischarge InertCans
_ EqCt
_ = Maybe (CtEvidence, SwapFlag)
forall a. Maybe a
Nothing
tryQCsIrredEqCt :: IrredCt -> SolverStage ()
tryQCsIrredEqCt :: IrredCt -> SolverStage ()
tryQCsIrredEqCt irred :: IrredCt
irred@(IrredCt { ir_ev :: IrredCt -> CtEvidence
ir_ev = CtEvidence
ev })
| EqPred EqRel
eq_rel TcType
t1 TcType
t2 <- TcType -> Pred
classifyPredType (CtEvidence -> TcType
ctEvPred CtEvidence
ev)
= Ct -> EqRel -> TcType -> TcType -> SolverStage ()
lookup_eq_in_qcis (IrredCt -> Ct
CIrredCan IrredCt
irred) EqRel
eq_rel TcType
t1 TcType
t2
| Bool
otherwise
= String -> SDoc -> SolverStage ()
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"solveIrredEquality" (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev)
tryQCsEqCt :: EqCt -> SolverStage ()
tryQCsEqCt :: EqCt -> SolverStage ()
tryQCsEqCt work_item :: EqCt
work_item@(EqCt { eq_lhs :: EqCt -> CanEqLHS
eq_lhs = CanEqLHS
lhs, eq_rhs :: EqCt -> TcType
eq_rhs = TcType
rhs, eq_eq_rel :: EqCt -> EqRel
eq_eq_rel = EqRel
eq_rel })
= Ct -> EqRel -> TcType -> TcType -> SolverStage ()
lookup_eq_in_qcis (EqCt -> Ct
CEqCan EqCt
work_item) EqRel
eq_rel (CanEqLHS -> TcType
canEqLHSType CanEqLHS
lhs) TcType
rhs
lookup_eq_in_qcis :: Ct -> EqRel -> TcType -> TcType -> SolverStage ()
lookup_eq_in_qcis :: Ct -> EqRel -> TcType -> TcType -> SolverStage ()
lookup_eq_in_qcis Ct
work_ct EqRel
eq_rel TcType
lhs TcType
rhs
= TcS (StopOrContinue ()) -> SolverStage ()
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue ()) -> SolverStage ())
-> TcS (StopOrContinue ()) -> SolverStage ()
forall a b. (a -> b) -> a -> b
$
do { ev_binds_var <- TcS EvBindsVar
getTcEvBindsVar
; ics <- getInertCans
; if isWanted ev
&& not (null (inert_insts ics))
&& not (isCoEvBindsVar ev_binds_var)
then try_for_qci
else continueWith () }
where
ev :: CtEvidence
ev = Ct -> CtEvidence
ctEvidence Ct
work_ct
loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
role :: Role
role = EqRel -> Role
eqRelRole EqRel
eq_rel
try_for_qci :: TcS (StopOrContinue ())
try_for_qci
| Just (Class
cls, [TcType]
tys) <- EqRel -> TcType -> TcType -> Maybe (Class, [TcType])
boxEqPred EqRel
eq_rel TcType
lhs TcType
rhs
= do { res <- TcType -> CtLoc -> TcS ClsInstResult
matchLocalInst (Class -> [TcType] -> TcType
mkClassPred Class
cls [TcType]
tys) CtLoc
loc
; traceTcS "lookup_irred_in_qcis:1" (ppr (mkClassPred cls tys))
; case res of
OneInst { cir_mk_ev :: ClsInstResult -> [EvExpr] -> EvTerm
cir_mk_ev = [EvExpr] -> EvTerm
mk_ev }
-> CtEvidence -> ClsInstResult -> TcS (StopOrContinue ())
forall a. CtEvidence -> ClsInstResult -> TcS (StopOrContinue a)
chooseInstance CtEvidence
ev (ClsInstResult
res { cir_mk_ev = mk_eq_ev cls tys mk_ev })
ClsInstResult
_ -> TcS (StopOrContinue ())
try_swapping }
| Bool
otherwise
= () -> TcS (StopOrContinue ())
forall a. a -> TcS (StopOrContinue a)
continueWith ()
try_swapping :: TcS (StopOrContinue ())
try_swapping
| Just (Class
cls, [TcType]
tys) <- EqRel -> TcType -> TcType -> Maybe (Class, [TcType])
boxEqPred EqRel
eq_rel TcType
rhs TcType
lhs
= do { res <- TcType -> CtLoc -> TcS ClsInstResult
matchLocalInst (Class -> [TcType] -> TcType
mkClassPred Class
cls [TcType]
tys) CtLoc
loc
; traceTcS "lookup_irred_in_qcis:2" (ppr (mkClassPred cls tys))
; case res of
OneInst { cir_mk_ev :: ClsInstResult -> [EvExpr] -> EvTerm
cir_mk_ev = [EvExpr] -> EvTerm
mk_ev }
-> do { ev' <- RewriterSet
-> CtEvidence
-> SwapFlag
-> Reduction
-> Reduction
-> TcS CtEvidence
rewriteEqEvidence RewriterSet
emptyRewriterSet CtEvidence
ev SwapFlag
IsSwapped
(Role -> TcType -> Reduction
mkReflRedn Role
role TcType
rhs) (Role -> TcType -> Reduction
mkReflRedn Role
role TcType
lhs)
; chooseInstance ev' (res { cir_mk_ev = mk_eq_ev cls tys mk_ev }) }
ClsInstResult
_ -> do { String -> SDoc -> TcS ()
traceTcS String
"lookup_irred_in_qcis:3" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
work_ct)
; () -> TcS (StopOrContinue ())
forall a. a -> TcS (StopOrContinue a)
continueWith () }}
| Bool
otherwise
= () -> TcS (StopOrContinue ())
forall a. a -> TcS (StopOrContinue a)
continueWith ()
mk_eq_ev :: Class -> [TcType] -> ([EvExpr] -> EvTerm) -> [EvExpr] -> EvTerm
mk_eq_ev Class
cls [TcType]
tys [EvExpr] -> EvTerm
mk_ev [EvExpr]
evs
| TcTyVar
sc_id : [TcTyVar]
rest <- Class -> [TcTyVar]
classSCSelIds Class
cls
= Bool -> EvTerm -> EvTerm
forall a. HasCallStack => Bool -> a -> a
assert ([TcTyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
rest) (EvTerm -> EvTerm) -> EvTerm -> EvTerm
forall a b. (a -> b) -> a -> b
$ case ([EvExpr] -> EvTerm
mk_ev [EvExpr]
evs) of
EvExpr EvExpr
e -> EvExpr -> EvTerm
EvExpr (TcTyVar -> EvExpr
forall b. TcTyVar -> Expr b
Var TcTyVar
sc_id EvExpr -> [TcType] -> EvExpr
forall b. Expr b -> [TcType] -> Expr b
`mkTyApps` [TcType]
tys EvExpr -> EvExpr -> EvExpr
forall b. Expr b -> Expr b -> Expr b
`App` EvExpr
e)
EvTerm
ev -> String -> SDoc -> EvTerm
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"mk_eq_ev" (EvTerm -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvTerm
ev)
| Bool
otherwise = String -> SDoc -> EvTerm
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"finishEqCt" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
work_ct)
tryFunDeps :: EqRel -> EqCt -> SolverStage ()
tryFunDeps :: EqRel -> EqCt -> SolverStage ()
tryFunDeps EqRel
eq_rel work_item :: EqCt
work_item@(EqCt { eq_lhs :: EqCt -> CanEqLHS
eq_lhs = CanEqLHS
lhs, eq_ev :: EqCt -> CtEvidence
eq_ev = CtEvidence
ev })
| EqRel
NomEq <- EqRel
eq_rel
, TyFamLHS TyCon
tc [TcType]
args <- CanEqLHS
lhs
= TcS (StopOrContinue ()) -> SolverStage ()
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue ()) -> SolverStage ())
-> TcS (StopOrContinue ()) -> SolverStage ()
forall a b. (a -> b) -> a -> b
$
do { inerts <- TcS InertCans
getInertCans
; imp1 <- improveLocalFunEqs inerts tc args work_item
; imp2 <- improveTopFunEqs tc args work_item
; if (imp1 || imp2)
then startAgainWith (mkNonCanonical ev)
else continueWith () }
| Bool
otherwise
= () -> SolverStage ()
forall a. a -> SolverStage a
nopStage ()
improveTopFunEqs :: TyCon -> [TcType] -> EqCt -> TcS Bool
improveTopFunEqs :: TyCon -> [TcType] -> EqCt -> TcS Bool
improveTopFunEqs TyCon
fam_tc [TcType]
args (EqCt { eq_ev :: EqCt -> CtEvidence
eq_ev = CtEvidence
ev, eq_rhs :: EqCt -> TcType
eq_rhs = TcType
rhs_ty })
| CtEvidence -> Bool
isGiven CtEvidence
ev = TyCon -> [TcType] -> CtEvidence -> TcType -> TcS Bool
improveGivenTopFunEqs TyCon
fam_tc [TcType]
args CtEvidence
ev TcType
rhs_ty
| Bool
otherwise = TyCon -> [TcType] -> CtEvidence -> TcType -> TcS Bool
improveWantedTopFunEqs TyCon
fam_tc [TcType]
args CtEvidence
ev TcType
rhs_ty
improveGivenTopFunEqs :: TyCon -> [TcType] -> CtEvidence -> Xi -> TcS Bool
improveGivenTopFunEqs :: TyCon -> [TcType] -> CtEvidence -> TcType -> TcS Bool
improveGivenTopFunEqs TyCon
fam_tc [TcType]
args CtEvidence
ev TcType
rhs_ty
| Just BuiltInSynFamily
ops <- TyCon -> Maybe BuiltInSynFamily
isBuiltInSynFamTyCon_maybe TyCon
fam_tc
= do { String -> SDoc -> TcS ()
traceTcS String
"improveGivenTopFunEqs" (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
fam_tc SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [TcType] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcType]
args SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
rhs_ty)
; CtLoc -> [(Role, TcCoercion)] -> TcS ()
emitNewGivens (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev) ([(Role, TcCoercion)] -> TcS ()) -> [(Role, TcCoercion)] -> TcS ()
forall a b. (a -> b) -> a -> b
$
[ (Role
Nominal, TcCoercion
new_co)
| (CoAxiomRule
ax, TypeEqn
_) <- BuiltInSynFamily
-> TyCon -> [TcType] -> TcType -> [(CoAxiomRule, TypeEqn)]
tryInteractTopFam BuiltInSynFamily
ops TyCon
fam_tc [TcType]
args TcType
rhs_ty
, let new_co :: TcCoercion
new_co = CoAxiomRule -> [TcCoercion] -> TcCoercion
mkAxiomCo CoAxiomRule
ax [TcCoercion
given_co] ]
; Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False }
| Bool
otherwise
= Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
where
TcCoercion
given_co :: Coercion = HasDebugCallStack => CtEvidence -> TcCoercion
CtEvidence -> TcCoercion
ctEvCoercion CtEvidence
ev
improveWantedTopFunEqs :: TyCon -> [TcType] -> CtEvidence -> Xi -> TcS Bool
improveWantedTopFunEqs :: TyCon -> [TcType] -> CtEvidence -> TcType -> TcS Bool
improveWantedTopFunEqs TyCon
fam_tc [TcType]
args CtEvidence
ev TcType
rhs_ty
= do { eqns <- TyCon -> [TcType] -> TcType -> TcS [TypeEqn]
improve_wanted_top_fun_eqs TyCon
fam_tc [TcType]
args TcType
rhs_ty
; traceTcS "improveTopFunEqs" (vcat [ ppr fam_tc <+> ppr args <+> ppr rhs_ty
, ppr eqns ])
; unifyFunDeps ev Nominal $ \UnifyEnv
uenv ->
UnifyEnv -> [TypeEqn] -> TcM ()
uPairsTcM (UnifyEnv -> UnifyEnv
bump_depth UnifyEnv
uenv) ([TypeEqn] -> [TypeEqn]
forall a. [a] -> [a]
reverse [TypeEqn]
eqns) }
where
bump_depth :: UnifyEnv -> UnifyEnv
bump_depth UnifyEnv
env = UnifyEnv
env { u_loc = bumpCtLocDepth (u_loc env) }
improve_wanted_top_fun_eqs :: TyCon -> [TcType] -> Xi
-> TcS [TypeEqn]
improve_wanted_top_fun_eqs :: TyCon -> [TcType] -> TcType -> TcS [TypeEqn]
improve_wanted_top_fun_eqs TyCon
fam_tc [TcType]
lhs_tys TcType
rhs_ty
| Just BuiltInSynFamily
ops <- TyCon -> Maybe BuiltInSynFamily
isBuiltInSynFamTyCon_maybe TyCon
fam_tc
= [TypeEqn] -> TcS [TypeEqn]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (((CoAxiomRule, TypeEqn) -> TypeEqn)
-> [(CoAxiomRule, TypeEqn)] -> [TypeEqn]
forall a b. (a -> b) -> [a] -> [b]
map (CoAxiomRule, TypeEqn) -> TypeEqn
forall a b. (a, b) -> b
snd ([(CoAxiomRule, TypeEqn)] -> [TypeEqn])
-> [(CoAxiomRule, TypeEqn)] -> [TypeEqn]
forall a b. (a -> b) -> a -> b
$ BuiltInSynFamily
-> TyCon -> [TcType] -> TcType -> [(CoAxiomRule, TypeEqn)]
tryInteractTopFam BuiltInSynFamily
ops TyCon
fam_tc [TcType]
lhs_tys TcType
rhs_ty)
| Injective [Bool]
inj_args <- TyCon -> Injectivity
tyConInjectivityInfo TyCon
fam_tc
= do { fam_envs <- TcS (FamInstEnv, FamInstEnv)
getFamInstEnvs
; top_eqns <- improve_injective_wanted_top fam_envs inj_args fam_tc lhs_tys rhs_ty
; let local_eqns = [Bool] -> TyCon -> [TcType] -> TcType -> [TypeEqn]
improve_injective_wanted_famfam [Bool]
inj_args TyCon
fam_tc [TcType]
lhs_tys TcType
rhs_ty
; return (local_eqns ++ top_eqns) }
| Bool
otherwise
= [TypeEqn] -> TcS [TypeEqn]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return []
improve_injective_wanted_top :: FamInstEnvs -> [Bool] -> TyCon -> [TcType] -> Xi -> TcS [TypeEqn]
improve_injective_wanted_top :: (FamInstEnv, FamInstEnv)
-> [Bool] -> TyCon -> [TcType] -> TcType -> TcS [TypeEqn]
improve_injective_wanted_top (FamInstEnv, FamInstEnv)
fam_envs [Bool]
inj_args TyCon
fam_tc [TcType]
lhs_tys TcType
rhs_ty
= (CoAxBranch -> TcS [TypeEqn]) -> [CoAxBranch] -> TcS [TypeEqn]
forall (m :: * -> *) (f :: * -> *) a b.
(Monad m, Traversable f) =>
(a -> m [b]) -> f a -> m [b]
concatMapM CoAxBranch -> TcS [TypeEqn]
do_one [CoAxBranch]
branches
where
branches :: [CoAxBranch]
branches :: [CoAxBranch]
branches | TyCon -> Bool
isOpenTypeFamilyTyCon TyCon
fam_tc
, let fam_insts :: [FamInst]
fam_insts = (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
lookupFamInstEnvByTyCon (FamInstEnv, FamInstEnv)
fam_envs TyCon
fam_tc
= (FamInst -> [CoAxBranch]) -> [FamInst] -> [CoAxBranch]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Branches Unbranched -> [CoAxBranch]
forall (br :: BranchFlag). Branches br -> [CoAxBranch]
fromBranches (Branches Unbranched -> [CoAxBranch])
-> (FamInst -> Branches Unbranched) -> FamInst -> [CoAxBranch]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoAxiom Unbranched -> Branches Unbranched
forall (br :: BranchFlag). CoAxiom br -> Branches br
coAxiomBranches (CoAxiom Unbranched -> Branches Unbranched)
-> (FamInst -> CoAxiom Unbranched)
-> FamInst
-> Branches Unbranched
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FamInst -> CoAxiom Unbranched
fi_axiom) [FamInst]
fam_insts
| Just CoAxiom Branched
ax <- TyCon -> Maybe (CoAxiom Branched)
isClosedSynFamilyTyConWithAxiom_maybe TyCon
fam_tc
= Branches Branched -> [CoAxBranch]
forall (br :: BranchFlag). Branches br -> [CoAxBranch]
fromBranches (CoAxiom Branched -> Branches Branched
forall (br :: BranchFlag). CoAxiom br -> Branches br
coAxiomBranches CoAxiom Branched
ax)
| Bool
otherwise
= []
do_one :: CoAxBranch -> TcS [TypeEqn]
do_one :: CoAxBranch -> TcS [TypeEqn]
do_one branch :: CoAxBranch
branch@(CoAxBranch { cab_tvs :: CoAxBranch -> [TcTyVar]
cab_tvs = [TcTyVar]
branch_tvs, cab_lhs :: CoAxBranch -> [TcType]
cab_lhs = [TcType]
branch_lhs_tys, cab_rhs :: CoAxBranch -> TcType
cab_rhs = TcType
branch_rhs })
| let in_scope1 :: InScopeSet
in_scope1 = InScopeSet
in_scope InScopeSet -> [TcTyVar] -> InScopeSet
`extendInScopeSetList` [TcTyVar]
branch_tvs
, Just Subst
subst <- Bool -> InScopeSet -> TcType -> TcType -> Maybe Subst
tcUnifyTyWithTFs Bool
False InScopeSet
in_scope1 TcType
branch_rhs TcType
rhs_ty
= do { let inSubst :: TcTyVar -> Bool
inSubst TcTyVar
tv = TcTyVar
tv TcTyVar -> VarEnv TcType -> Bool
forall a. TcTyVar -> VarEnv a -> Bool
`elemVarEnv` Subst -> VarEnv TcType
getTvSubstEnv Subst
subst
unsubstTvs :: [TcTyVar]
unsubstTvs = (TcTyVar -> Bool) -> [TcTyVar] -> [TcTyVar]
forall a. (a -> Bool) -> [a] -> [a]
filterOut TcTyVar -> Bool
inSubst [TcTyVar]
branch_tvs
; subst <- Subst -> [TcTyVar] -> TcS Subst
instFlexiX Subst
subst [TcTyVar]
unsubstTvs
; if apartnessCheck (substTys subst branch_lhs_tys) branch
then return (mkInjectivityEqns inj_args (map (substTy subst) branch_lhs_tys) lhs_tys)
else return [] }
| Bool
otherwise
= [TypeEqn] -> TcS [TypeEqn]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return []
in_scope :: InScopeSet
in_scope = TyCoVarSet -> InScopeSet
mkInScopeSet (TcType -> TyCoVarSet
tyCoVarsOfType TcType
rhs_ty)
improve_injective_wanted_famfam :: [Bool] -> TyCon -> [TcType] -> Xi -> [TypeEqn]
improve_injective_wanted_famfam :: [Bool] -> TyCon -> [TcType] -> TcType -> [TypeEqn]
improve_injective_wanted_famfam [Bool]
inj_args TyCon
fam_tc [TcType]
lhs_tys TcType
rhs_ty
| Just (TyCon
tc, [TcType]
rhs_tys) <- HasDebugCallStack => TcType -> Maybe (TyCon, [TcType])
TcType -> Maybe (TyCon, [TcType])
tcSplitTyConApp_maybe TcType
rhs_ty
, TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
fam_tc
= [Bool] -> [TcType] -> [TcType] -> [TypeEqn]
mkInjectivityEqns [Bool]
inj_args [TcType]
lhs_tys [TcType]
rhs_tys
| Bool
otherwise
= []
mkInjectivityEqns :: [Bool] -> [TcType] -> [TcType] -> [TypeEqn]
mkInjectivityEqns :: [Bool] -> [TcType] -> [TcType] -> [TypeEqn]
mkInjectivityEqns [Bool]
inj_args [TcType]
lhs_args [TcType]
rhs_args
= [ TcType -> TcType -> TypeEqn
forall a. a -> a -> Pair a
Pair TcType
lhs_arg TcType
rhs_arg | (Bool
True, TcType
lhs_arg, TcType
rhs_arg) <- [Bool] -> [TcType] -> [TcType] -> [(Bool, TcType, TcType)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Bool]
inj_args [TcType]
lhs_args [TcType]
rhs_args ]
improveLocalFunEqs :: InertCans
-> TyCon -> [TcType] -> EqCt
-> TcS Bool
improveLocalFunEqs :: InertCans -> TyCon -> [TcType] -> EqCt -> TcS Bool
improveLocalFunEqs InertCans
inerts TyCon
fam_tc [TcType]
args (EqCt { eq_ev :: EqCt -> CtEvidence
eq_ev = CtEvidence
work_ev, eq_rhs :: EqCt -> TcType
eq_rhs = TcType
rhs })
| CtEvidence -> Bool
isGiven CtEvidence
work_ev = [EqCt] -> TyCon -> [TcType] -> CtEvidence -> TcType -> TcS Bool
improveGivenLocalFunEqs [EqCt]
funeqs_for_tc TyCon
fam_tc [TcType]
args CtEvidence
work_ev TcType
rhs
| Bool
otherwise = [EqCt] -> TyCon -> [TcType] -> CtEvidence -> TcType -> TcS Bool
improveWantedLocalFunEqs [EqCt]
funeqs_for_tc TyCon
fam_tc [TcType]
args CtEvidence
work_ev TcType
rhs
where
funeqs :: InertFunEqs
funeqs = InertCans -> InertFunEqs
inert_funeqs InertCans
inerts
funeqs_for_tc :: [EqCt]
funeqs_for_tc :: [EqCt]
funeqs_for_tc = [ EqCt
funeq_ct | [EqCt]
equal_ct_list <- InertFunEqs -> TyCon -> [[EqCt]]
forall a. FunEqMap a -> TyCon -> [a]
findFunEqsByTyCon InertFunEqs
funeqs TyCon
fam_tc
, EqCt
funeq_ct <- [EqCt]
equal_ct_list
, EqRel
NomEq EqRel -> EqRel -> Bool
forall a. Eq a => a -> a -> Bool
== EqCt -> EqRel
eq_eq_rel EqCt
funeq_ct ]
improveGivenLocalFunEqs :: [EqCt]
-> TyCon -> [TcType] -> CtEvidence -> Xi
-> TcS Bool
improveGivenLocalFunEqs :: [EqCt] -> TyCon -> [TcType] -> CtEvidence -> TcType -> TcS Bool
improveGivenLocalFunEqs [EqCt]
funeqs_for_tc TyCon
fam_tc [TcType]
work_args CtEvidence
work_ev TcType
work_rhs
| Just BuiltInSynFamily
ops <- TyCon -> Maybe BuiltInSynFamily
isBuiltInSynFamTyCon_maybe TyCon
fam_tc
= do { (EqCt -> TcS ()) -> [EqCt] -> TcS ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (BuiltInSynFamily -> EqCt -> TcS ()
do_one BuiltInSynFamily
ops) [EqCt]
funeqs_for_tc
; Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False }
| Bool
otherwise
= Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
where
TcCoercion
given_co :: Coercion = HasDebugCallStack => CtEvidence -> TcCoercion
CtEvidence -> TcCoercion
ctEvCoercion CtEvidence
work_ev
do_one :: BuiltInSynFamily -> EqCt -> TcS ()
do_one :: BuiltInSynFamily -> EqCt -> TcS ()
do_one BuiltInSynFamily
ops EqCt { eq_ev :: EqCt -> CtEvidence
eq_ev = CtEvidence
inert_ev, eq_lhs :: EqCt -> CanEqLHS
eq_lhs = CanEqLHS
inert_lhs, eq_rhs :: EqCt -> TcType
eq_rhs = TcType
inert_rhs }
| CtEvidence -> Bool
isGiven CtEvidence
inert_ev
, TyFamLHS TyCon
_ [TcType]
inert_args <- CanEqLHS
inert_lhs
, TcType
work_rhs HasDebugCallStack => TcType -> TcType -> Bool
TcType -> TcType -> Bool
`tcEqType` TcType
inert_rhs
,
let pairs :: [(CoAxiomRule, TypeEqn)]
pairs :: [(CoAxiomRule, TypeEqn)]
pairs = BuiltInSynFamily
-> TyCon -> [TcType] -> [TcType] -> [(CoAxiomRule, TypeEqn)]
tryInteractInertFam BuiltInSynFamily
ops TyCon
fam_tc [TcType]
work_args [TcType]
inert_args
, Bool -> Bool
not ([(CoAxiomRule, TypeEqn)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(CoAxiomRule, TypeEqn)]
pairs)
= do { String -> SDoc -> TcS ()
traceTcS String
"improveGivenLocalFunEqs" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat[ TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
fam_tc SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [TcType] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcType]
work_args
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"work_ev" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
work_ev
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"inert_ev" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
inert_ev
, TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
work_rhs
, [(CoAxiomRule, TypeEqn)] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(CoAxiomRule, TypeEqn)]
pairs ])
; CtLoc -> [(Role, TcCoercion)] -> TcS ()
emitNewGivens (CtEvidence -> CtLoc
ctEvLoc CtEvidence
inert_ev) (((CoAxiomRule, TypeEqn) -> (Role, TcCoercion))
-> [(CoAxiomRule, TypeEqn)] -> [(Role, TcCoercion)]
forall a b. (a -> b) -> [a] -> [b]
map (CoAxiomRule, TypeEqn) -> (Role, TcCoercion)
mk_ax_co [(CoAxiomRule, TypeEqn)]
pairs) }
where
inert_co :: TcCoercion
inert_co = HasDebugCallStack => CtEvidence -> TcCoercion
CtEvidence -> TcCoercion
ctEvCoercion CtEvidence
inert_ev
mk_ax_co :: (CoAxiomRule, TypeEqn) -> (Role, TcCoercion)
mk_ax_co (CoAxiomRule
ax,TypeEqn
_) = (Role
Nominal, CoAxiomRule -> [TcCoercion] -> TcCoercion
mkAxiomCo CoAxiomRule
ax [TcCoercion
combined_co])
where
combined_co :: TcCoercion
combined_co = TcCoercion
given_co HasDebugCallStack => TcCoercion -> TcCoercion -> TcCoercion
TcCoercion -> TcCoercion -> TcCoercion
`mkTransCo` TcCoercion -> TcCoercion
mkSymCo TcCoercion
inert_co
do_one BuiltInSynFamily
_ EqCt
_ = () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
improveWantedLocalFunEqs
:: [EqCt]
-> TyCon -> [TcType] -> CtEvidence -> Xi
-> TcS Bool
improveWantedLocalFunEqs :: [EqCt] -> TyCon -> [TcType] -> CtEvidence -> TcType -> TcS Bool
improveWantedLocalFunEqs [EqCt]
funeqs_for_tc TyCon
fam_tc [TcType]
args CtEvidence
work_ev TcType
rhs
| [FunDepEqn (CtLoc, RewriterSet)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FunDepEqn (CtLoc, RewriterSet)]
improvement_eqns
= Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
| Bool
otherwise
= do { String -> SDoc -> TcS ()
traceTcS String
"interactFunEq improvements: " (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Eqns:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [FunDepEqn (CtLoc, RewriterSet)] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [FunDepEqn (CtLoc, RewriterSet)]
improvement_eqns
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Candidates:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [EqCt] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [EqCt]
funeqs_for_tc ]
; CtEvidence -> [FunDepEqn (CtLoc, RewriterSet)] -> TcS Bool
emitFunDepWanteds CtEvidence
work_ev [FunDepEqn (CtLoc, RewriterSet)]
improvement_eqns }
where
work_loc :: CtLoc
work_loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
work_ev
work_pred :: TcType
work_pred = CtEvidence -> TcType
ctEvPred CtEvidence
work_ev
fam_inj_info :: Injectivity
fam_inj_info = TyCon -> Injectivity
tyConInjectivityInfo TyCon
fam_tc
improvement_eqns :: [FunDepEqn (CtLoc, RewriterSet)]
improvement_eqns :: [FunDepEqn (CtLoc, RewriterSet)]
improvement_eqns
| Just BuiltInSynFamily
ops <- TyCon -> Maybe BuiltInSynFamily
isBuiltInSynFamTyCon_maybe TyCon
fam_tc
=
(EqCt -> [FunDepEqn (CtLoc, RewriterSet)])
-> [EqCt] -> [FunDepEqn (CtLoc, RewriterSet)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (BuiltInSynFamily
-> TcType -> EqCt -> [FunDepEqn (CtLoc, RewriterSet)]
do_one_built_in BuiltInSynFamily
ops TcType
rhs) [EqCt]
funeqs_for_tc
| Injective [Bool]
injective_args <- Injectivity
fam_inj_info
=
(EqCt -> [FunDepEqn (CtLoc, RewriterSet)])
-> [EqCt] -> [FunDepEqn (CtLoc, RewriterSet)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Bool] -> TcType -> EqCt -> [FunDepEqn (CtLoc, RewriterSet)]
do_one_injective [Bool]
injective_args TcType
rhs) [EqCt]
funeqs_for_tc
| Bool
otherwise
= []
do_one_built_in :: BuiltInSynFamily
-> TcType -> EqCt -> [FunDepEqn (CtLoc, RewriterSet)]
do_one_built_in BuiltInSynFamily
ops TcType
rhs (EqCt { eq_lhs :: EqCt -> CanEqLHS
eq_lhs = TyFamLHS TyCon
_ [TcType]
iargs, eq_rhs :: EqCt -> TcType
eq_rhs = TcType
irhs, eq_ev :: EqCt -> CtEvidence
eq_ev = CtEvidence
inert_ev })
| TcType
irhs HasDebugCallStack => TcType -> TcType -> Bool
TcType -> TcType -> Bool
`tcEqType` TcType
rhs
= CtEvidence -> [TypeEqn] -> [FunDepEqn (CtLoc, RewriterSet)]
mk_fd_eqns CtEvidence
inert_ev (((CoAxiomRule, TypeEqn) -> TypeEqn)
-> [(CoAxiomRule, TypeEqn)] -> [TypeEqn]
forall a b. (a -> b) -> [a] -> [b]
map (CoAxiomRule, TypeEqn) -> TypeEqn
forall a b. (a, b) -> b
snd ([(CoAxiomRule, TypeEqn)] -> [TypeEqn])
-> [(CoAxiomRule, TypeEqn)] -> [TypeEqn]
forall a b. (a -> b) -> a -> b
$ BuiltInSynFamily
-> TyCon -> [TcType] -> [TcType] -> [(CoAxiomRule, TypeEqn)]
tryInteractInertFam BuiltInSynFamily
ops TyCon
fam_tc [TcType]
args [TcType]
iargs)
| Bool
otherwise
= []
do_one_built_in BuiltInSynFamily
_ TcType
_ EqCt
_ = String -> SDoc -> [FunDepEqn (CtLoc, RewriterSet)]
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"interactFunEq 1" (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
fam_tc)
do_one_injective :: [Bool] -> TcType -> EqCt -> [FunDepEqn (CtLoc, RewriterSet)]
do_one_injective [Bool]
inj_args TcType
rhs (EqCt { eq_lhs :: EqCt -> CanEqLHS
eq_lhs = TyFamLHS TyCon
_ [TcType]
inert_args
, eq_rhs :: EqCt -> TcType
eq_rhs = TcType
irhs, eq_ev :: EqCt -> CtEvidence
eq_ev = CtEvidence
inert_ev })
| TcType
rhs HasDebugCallStack => TcType -> TcType -> Bool
TcType -> TcType -> Bool
`tcEqType` TcType
irhs
= CtEvidence -> [TypeEqn] -> [FunDepEqn (CtLoc, RewriterSet)]
mk_fd_eqns CtEvidence
inert_ev ([TypeEqn] -> [FunDepEqn (CtLoc, RewriterSet)])
-> [TypeEqn] -> [FunDepEqn (CtLoc, RewriterSet)]
forall a b. (a -> b) -> a -> b
$ [Bool] -> [TcType] -> [TcType] -> [TypeEqn]
mkInjectivityEqns [Bool]
inj_args [TcType]
args [TcType]
inert_args
| Bool
otherwise
= []
do_one_injective [Bool]
_ TcType
_ EqCt
_ = String -> SDoc -> [FunDepEqn (CtLoc, RewriterSet)]
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"interactFunEq 2" (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
fam_tc)
mk_fd_eqns :: CtEvidence -> [TypeEqn] -> [FunDepEqn (CtLoc, RewriterSet)]
mk_fd_eqns :: CtEvidence -> [TypeEqn] -> [FunDepEqn (CtLoc, RewriterSet)]
mk_fd_eqns CtEvidence
inert_ev [TypeEqn]
eqns
| [TypeEqn] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeEqn]
eqns = []
| Bool
otherwise = [ FDEqn { fd_qtvs :: [TcTyVar]
fd_qtvs = [], fd_eqs :: [TypeEqn]
fd_eqs = [TypeEqn]
eqns
, fd_loc :: (CtLoc, RewriterSet)
fd_loc = (CtLoc
loc, RewriterSet
inert_rewriters) } ]
where
initial_loc :: CtLoc
initial_loc
| CtEvidence -> Bool
isGiven CtEvidence
work_ev = CtLoc
inert_loc
| Bool
otherwise = CtLoc
work_loc
eqn_orig :: CtOrigin
eqn_orig = TcType
-> CtOrigin
-> RealSrcSpan
-> TcType
-> CtOrigin
-> RealSrcSpan
-> CtOrigin
InjTFOrigin1 TcType
work_pred (CtLoc -> CtOrigin
ctLocOrigin CtLoc
work_loc) (CtLoc -> RealSrcSpan
ctLocSpan CtLoc
work_loc)
TcType
inert_pred (CtLoc -> CtOrigin
ctLocOrigin CtLoc
inert_loc) (CtLoc -> RealSrcSpan
ctLocSpan CtLoc
inert_loc)
eqn_loc :: CtLoc
eqn_loc = CtLoc -> CtOrigin -> CtLoc
setCtLocOrigin CtLoc
initial_loc CtOrigin
eqn_orig
inert_pred :: TcType
inert_pred = CtEvidence -> TcType
ctEvPred CtEvidence
inert_ev
inert_loc :: CtLoc
inert_loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
inert_ev
inert_rewriters :: RewriterSet
inert_rewriters = CtEvidence -> RewriterSet
ctEvRewriters CtEvidence
inert_ev
loc :: CtLoc
loc = CtLoc
eqn_loc { ctl_depth = ctl_depth inert_loc `maxSubGoalDepth`
ctl_depth work_loc }