{-# LANGUAGE DeriveFunctor #-}
module GHC.Tc.Instance.FunDeps
( FunDepEqn(..)
, pprEquation
, improveFromInstEnv
, improveFromAnother
, checkInstCoverage
, checkFunDeps
, pprFundeps
, instFD, closeWrtFunDeps
)
where
import GHC.Prelude
import GHC.Types.Var
import GHC.Core.Class
import GHC.Core.Predicate
import GHC.Core.Type
import GHC.Core.RoughMap( RoughMatchTc(..) )
import GHC.Core.Coercion.Axiom( TypeEqn )
import GHC.Core.Unify
import GHC.Core.InstEnv
import GHC.Core.TyCo.FVs
import GHC.Core.TyCo.Compare( eqTypes, eqType )
import GHC.Tc.Errors.Types ( CoverageProblem(..), FailedCoverageCondition(..) )
import GHC.Tc.Types.Constraint ( isUnsatisfiableCt_maybe )
import GHC.Tc.Utils.TcType( transSuperClasses )
import GHC.Types.Var.Set
import GHC.Types.Var.Env
import GHC.Utils.Outputable
import GHC.Utils.FV
import GHC.Utils.Error( Validity'(..), allValid )
import GHC.Utils.Misc
import GHC.Utils.Panic
import GHC.Data.Pair ( Pair(..) )
import Data.List ( nubBy )
import Data.Maybe ( isJust, isNothing )
data FunDepEqn loc
= FDEqn { forall loc. FunDepEqn loc -> [TyVar]
fd_qtvs :: [TyVar]
, forall loc. FunDepEqn loc -> [TypeEqn]
fd_eqs :: [TypeEqn]
, forall loc. FunDepEqn loc -> loc
fd_loc :: loc }
deriving (forall a b. (a -> b) -> FunDepEqn a -> FunDepEqn b)
-> (forall a b. a -> FunDepEqn b -> FunDepEqn a)
-> Functor FunDepEqn
forall a b. a -> FunDepEqn b -> FunDepEqn a
forall a b. (a -> b) -> FunDepEqn a -> FunDepEqn b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> FunDepEqn a -> FunDepEqn b
fmap :: forall a b. (a -> b) -> FunDepEqn a -> FunDepEqn b
$c<$ :: forall a b. a -> FunDepEqn b -> FunDepEqn a
<$ :: forall a b. a -> FunDepEqn b -> FunDepEqn a
Functor
instance Outputable (FunDepEqn a) where
ppr :: FunDepEqn a -> SDoc
ppr = FunDepEqn a -> SDoc
forall a. FunDepEqn a -> SDoc
pprEquation
pprEquation :: FunDepEqn a -> SDoc
pprEquation :: forall a. FunDepEqn a -> SDoc
pprEquation (FDEqn { fd_qtvs :: forall loc. FunDepEqn loc -> [TyVar]
fd_qtvs = [TyVar]
qtvs, fd_eqs :: forall loc. FunDepEqn loc -> [TypeEqn]
fd_eqs = [TypeEqn]
pairs })
= [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"forall" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
braces ((TyVar -> SDoc) -> [TyVar] -> SDoc
forall a. (a -> SDoc) -> [a] -> SDoc
pprWithCommas TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVar]
qtvs),
Int -> SDoc -> SDoc
nest Int
2 ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
t1 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
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
t2
| Pair Type
t1 Type
t2 <- [TypeEqn]
pairs])]
instFD :: FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
instFD :: FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
instFD ([TyVar]
ls,[TyVar]
rs) [TyVar]
tvs [Type]
tys
= ((TyVar -> Type) -> [TyVar] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map TyVar -> Type
lookup [TyVar]
ls, (TyVar -> Type) -> [TyVar] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map TyVar -> Type
lookup [TyVar]
rs)
where
env :: VarEnv Type
env = [TyVar] -> [Type] -> VarEnv Type
forall a. [TyVar] -> [a] -> VarEnv a
zipVarEnv [TyVar]
tvs [Type]
tys
lookup :: TyVar -> Type
lookup TyVar
tv = VarEnv Type -> TyVar -> Type
forall a. VarEnv a -> TyVar -> a
lookupVarEnv_NF VarEnv Type
env TyVar
tv
zipAndComputeFDEqs :: (Type -> Type -> Bool)
-> [Type] -> [Type]
-> [TypeEqn]
zipAndComputeFDEqs :: (Type -> Type -> Bool) -> [Type] -> [Type] -> [TypeEqn]
zipAndComputeFDEqs Type -> Type -> Bool
discard (Type
ty1:[Type]
tys1) (Type
ty2:[Type]
tys2)
| Type -> Type -> Bool
discard Type
ty1 Type
ty2 = (Type -> Type -> Bool) -> [Type] -> [Type] -> [TypeEqn]
zipAndComputeFDEqs Type -> Type -> Bool
discard [Type]
tys1 [Type]
tys2
| Bool
otherwise = Type -> Type -> TypeEqn
forall a. a -> a -> Pair a
Pair Type
ty1 Type
ty2 TypeEqn -> [TypeEqn] -> [TypeEqn]
forall a. a -> [a] -> [a]
: (Type -> Type -> Bool) -> [Type] -> [Type] -> [TypeEqn]
zipAndComputeFDEqs Type -> Type -> Bool
discard [Type]
tys1 [Type]
tys2
zipAndComputeFDEqs Type -> Type -> Bool
_ [Type]
_ [Type]
_ = []
improveFromAnother :: loc
-> PredType
-> PredType
-> [FunDepEqn loc]
improveFromAnother :: forall loc. loc -> Type -> Type -> [FunDepEqn loc]
improveFromAnother loc
loc Type
pred1 Type
pred2
| Just (Class
cls1, [Type]
tys1) <- Type -> Maybe (Class, [Type])
getClassPredTys_maybe Type
pred1
, Just (Class
cls2, [Type]
tys2) <- Type -> Maybe (Class, [Type])
getClassPredTys_maybe Type
pred2
, Class
cls1 Class -> Class -> Bool
forall a. Eq a => a -> a -> Bool
== Class
cls2
= [ FDEqn { fd_qtvs :: [TyVar]
fd_qtvs = [], fd_eqs :: [TypeEqn]
fd_eqs = [TypeEqn]
eqs, fd_loc :: loc
fd_loc = loc
loc }
| let ([TyVar]
cls_tvs, [FunDep TyVar]
cls_fds) = Class -> ([TyVar], [FunDep TyVar])
classTvsFds Class
cls1
, FunDep TyVar
fd <- [FunDep TyVar]
cls_fds
, let ([Type]
ltys1, [Type]
rs1) = FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
instFD FunDep TyVar
fd [TyVar]
cls_tvs [Type]
tys1
([Type]
ltys2, [Type]
rs2) = FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
instFD FunDep TyVar
fd [TyVar]
cls_tvs [Type]
tys2
, [Type] -> [Type] -> Bool
eqTypes [Type]
ltys1 [Type]
ltys2
, let eqs :: [TypeEqn]
eqs = (Type -> Type -> Bool) -> [Type] -> [Type] -> [TypeEqn]
zipAndComputeFDEqs HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
eqType [Type]
rs1 [Type]
rs2
, Bool -> Bool
not ([TypeEqn] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeEqn]
eqs) ]
improveFromAnother loc
_ Type
_ Type
_ = []
improveFromInstEnv :: InstEnvs
-> (ClsInst -> loc)
-> Class -> [Type]
-> [FunDepEqn loc]
improveFromInstEnv :: forall loc.
InstEnvs -> (ClsInst -> loc) -> Class -> [Type] -> [FunDepEqn loc]
improveFromInstEnv InstEnvs
inst_env ClsInst -> loc
mk_loc Class
cls [Type]
tys
= [ FDEqn { fd_qtvs :: [TyVar]
fd_qtvs = [TyVar]
meta_tvs, fd_eqs :: [TypeEqn]
fd_eqs = [TypeEqn]
eqs, fd_loc :: loc
fd_loc = ClsInst -> loc
mk_loc ClsInst
ispec }
| FunDep TyVar
fd <- [FunDep TyVar]
cls_fds
, let trimmed_tcs :: [RoughMatchTc]
trimmed_tcs = [TyVar] -> FunDep TyVar -> [RoughMatchTc] -> [RoughMatchTc]
trimRoughMatchTcs [TyVar]
cls_tvs FunDep TyVar
fd [RoughMatchTc]
rough_tcs
, ClsInst
ispec <- [ClsInst]
instances
, ([TyVar]
meta_tvs, [TypeEqn]
eqs) <- [TyVar]
-> FunDep TyVar
-> ClsInst
-> [Type]
-> [RoughMatchTc]
-> [([TyVar], [TypeEqn])]
improveClsFD [TyVar]
cls_tvs FunDep TyVar
fd ClsInst
ispec
[Type]
tys [RoughMatchTc]
trimmed_tcs
]
where
([TyVar]
cls_tvs, [FunDep TyVar]
cls_fds) = Class -> ([TyVar], [FunDep TyVar])
classTvsFds Class
cls
instances :: [ClsInst]
instances = InstEnvs -> Class -> [ClsInst]
classInstances InstEnvs
inst_env Class
cls
rough_tcs :: [RoughMatchTc]
rough_tcs = Name -> RoughMatchTc
RM_KnownTc (Class -> Name
className Class
cls) RoughMatchTc -> [RoughMatchTc] -> [RoughMatchTc]
forall a. a -> [a] -> [a]
: [Type] -> [RoughMatchTc]
roughMatchTcs [Type]
tys
improveClsFD :: [TyVar] -> FunDep TyVar
-> ClsInst
-> [Type] -> [RoughMatchTc]
-> [([TyCoVar], [TypeEqn])]
improveClsFD :: [TyVar]
-> FunDep TyVar
-> ClsInst
-> [Type]
-> [RoughMatchTc]
-> [([TyVar], [TypeEqn])]
improveClsFD [TyVar]
clas_tvs FunDep TyVar
fd
(ClsInst { is_tvs :: ClsInst -> [TyVar]
is_tvs = [TyVar]
qtvs, is_tys :: ClsInst -> [Type]
is_tys = [Type]
tys_inst, is_tcs :: ClsInst -> [RoughMatchTc]
is_tcs = [RoughMatchTc]
rough_tcs_inst })
[Type]
tys_actual [RoughMatchTc]
rough_tcs_actual
| [RoughMatchTc] -> [RoughMatchTc] -> Bool
instanceCantMatch [RoughMatchTc]
rough_tcs_inst [RoughMatchTc]
rough_tcs_actual
= []
| Bool
otherwise
= Bool -> SDoc -> [([TyVar], [TypeEqn])] -> [([TyVar], [TypeEqn])]
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ([Type] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
equalLength [Type]
tys_inst [Type]
tys_actual Bool -> Bool -> Bool
&&
[Type] -> [TyVar] -> Bool
forall a b. [a] -> [b] -> Bool
equalLength [Type]
tys_inst [TyVar]
clas_tvs)
([Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys_inst SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys_actual) ([([TyVar], [TypeEqn])] -> [([TyVar], [TypeEqn])])
-> [([TyVar], [TypeEqn])] -> [([TyVar], [TypeEqn])]
forall a b. (a -> b) -> a -> b
$
case Subst -> [Type] -> [Type] -> Maybe Subst
tcMatchTyKisX Subst
init_subst [Type]
ltys1 [Type]
ltys2 of
Maybe Subst
Nothing -> []
Just Subst
subst | Maybe Subst -> Bool
forall a. Maybe a -> Bool
isJust (Subst -> [Type] -> [Type] -> Maybe Subst
tcMatchTyKisX Subst
subst [Type]
rtys1 [Type]
rtys2)
-> []
| [TypeEqn] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeEqn]
fdeqs
-> []
| Bool
otherwise
->
[([TyVar]
meta_tvs, [TypeEqn]
fdeqs)]
where
rtys1' :: [Type]
rtys1' = (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst) [Type]
rtys1
fdeqs :: [TypeEqn]
fdeqs = (Type -> Type -> Bool) -> [Type] -> [Type] -> [TypeEqn]
zipAndComputeFDEqs (\Type
_ Type
_ -> Bool
False) [Type]
rtys1' [Type]
rtys2
meta_tvs :: [TyVar]
meta_tvs = [ TyVar -> Type -> TyVar
setVarType TyVar
tv (HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst (TyVar -> Type
varType TyVar
tv))
| TyVar
tv <- [TyVar]
qtvs
, TyVar
tv TyVar -> Subst -> Bool
`notElemSubst` Subst
subst
, TyVar
tv TyVar -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
rtys1_tvs ]
where
init_subst :: Subst
init_subst = InScopeSet -> Subst
mkEmptySubst (InScopeSet -> Subst) -> InScopeSet -> Subst
forall a b. (a -> b) -> a -> b
$ TyCoVarSet -> InScopeSet
mkInScopeSet (TyCoVarSet -> InScopeSet) -> TyCoVarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$
[TyVar] -> TyCoVarSet
mkVarSet [TyVar]
qtvs TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` [Type] -> TyCoVarSet
tyCoVarsOfTypes [Type]
ltys2
([Type]
ltys1, [Type]
rtys1) = FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
instFD FunDep TyVar
fd [TyVar]
clas_tvs [Type]
tys_inst
([Type]
ltys2, [Type]
rtys2) = FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
instFD FunDep TyVar
fd [TyVar]
clas_tvs [Type]
tys_actual
rtys1_tvs :: TyCoVarSet
rtys1_tvs = [Type] -> TyCoVarSet
tyCoVarsOfTypes [Type]
rtys1
checkInstCoverage :: Bool
-> Class -> [PredType] -> [Type]
-> Validity' CoverageProblem
checkInstCoverage :: Bool -> Class -> [Type] -> [Type] -> Validity' CoverageProblem
checkInstCoverage Bool
be_liberal Class
clas [Type]
theta [Type]
inst_taus
| (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Maybe Type -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Type -> Bool) -> (Type -> Maybe Type) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe Type
isUnsatisfiableCt_maybe) [Type]
theta
= Validity' CoverageProblem
forall a. Validity' a
IsValid
| Bool
otherwise
= [Validity' CoverageProblem] -> Validity' CoverageProblem
forall a. [Validity' a] -> Validity' a
allValid ((FunDep TyVar -> Validity' CoverageProblem)
-> [FunDep TyVar] -> [Validity' CoverageProblem]
forall a b. (a -> b) -> [a] -> [b]
map FunDep TyVar -> Validity' CoverageProblem
fundep_ok [FunDep TyVar]
fds)
where
([TyVar]
tyvars, [FunDep TyVar]
fds) = Class -> ([TyVar], [FunDep TyVar])
classTvsFds Class
clas
fundep_ok :: FunDep TyVar -> Validity' CoverageProblem
fundep_ok FunDep TyVar
fd
| (TyCoVarSet -> Bool) -> Pair TyCoVarSet -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all TyCoVarSet -> Bool
isEmptyVarSet Pair TyCoVarSet
undetermined_tvs
= Validity' CoverageProblem
forall a. Validity' a
IsValid
| Bool
otherwise
= CoverageProblem -> Validity' CoverageProblem
forall a. a -> Validity' a
NotValid CoverageProblem
not_covered_msg
where
([Type]
ls,[Type]
rs) = FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
instFD FunDep TyVar
fd [TyVar]
tyvars [Type]
inst_taus
ls_tvs :: TyCoVarSet
ls_tvs = [Type] -> TyCoVarSet
tyCoVarsOfTypes [Type]
ls
rs_tvs :: Pair TyCoVarSet
rs_tvs = [Type] -> Pair TyCoVarSet
visVarsOfTypes [Type]
rs
undetermined_tvs :: Pair TyCoVarSet
undetermined_tvs | Bool
be_liberal = Pair TyCoVarSet
liberal_undet_tvs
| Bool
otherwise = Pair TyCoVarSet
conserv_undet_tvs
closed_ls_tvs :: TyCoVarSet
closed_ls_tvs = [Type] -> TyCoVarSet -> TyCoVarSet
closeWrtFunDeps [Type]
theta TyCoVarSet
ls_tvs
liberal_undet_tvs :: Pair TyCoVarSet
liberal_undet_tvs = (TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`minusVarSet` TyCoVarSet
closed_ls_tvs) (TyCoVarSet -> TyCoVarSet) -> Pair TyCoVarSet -> Pair TyCoVarSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair TyCoVarSet
rs_tvs
conserv_undet_tvs :: Pair TyCoVarSet
conserv_undet_tvs = (TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`minusVarSet` TyCoVarSet
ls_tvs) (TyCoVarSet -> TyCoVarSet) -> Pair TyCoVarSet -> Pair TyCoVarSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair TyCoVarSet
rs_tvs
not_covered_msg :: CoverageProblem
not_covered_msg =
CoverageProblem
{ not_covered_fundep :: FunDep TyVar
not_covered_fundep = FunDep TyVar
fd
, not_covered_fundep_inst :: FunDep Type
not_covered_fundep_inst = ([Type]
ls, [Type]
rs)
, not_covered_invis_vis_tvs :: Pair TyCoVarSet
not_covered_invis_vis_tvs = Pair TyCoVarSet
undetermined_tvs
, not_covered_liberal :: FailedCoverageCondition
not_covered_liberal =
if Bool
be_liberal
then FailedCoverageCondition
FailedLICC
else FailedICC
{ alsoFailedLICC :: Bool
alsoFailedLICC = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (TyCoVarSet -> Bool) -> Pair TyCoVarSet -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all TyCoVarSet -> Bool
isEmptyVarSet Pair TyCoVarSet
liberal_undet_tvs }
}
closeWrtFunDeps :: [PredType] -> TyCoVarSet -> TyCoVarSet
closeWrtFunDeps :: [Type] -> TyCoVarSet -> TyCoVarSet
closeWrtFunDeps [Type]
preds TyCoVarSet
fixed_tvs
| [(TyCoVarSet, TyCoVarSet)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(TyCoVarSet, TyCoVarSet)]
tv_fds = TyCoVarSet
fixed_tvs
| Bool
otherwise = Bool -> SDoc -> TyCoVarSet -> TyCoVarSet
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TyCoVarSet -> TyCoVarSet
closeOverKinds TyCoVarSet
fixed_tvs TyCoVarSet -> TyCoVarSet -> Bool
forall a. Eq a => a -> a -> Bool
== TyCoVarSet
fixed_tvs)
([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"closeWrtFunDeps: fixed_tvs is not closed over kinds"
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"fixed_tvs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TyCoVarSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCoVarSet
fixed_tvs
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"closure:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TyCoVarSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyCoVarSet -> TyCoVarSet
closeOverKinds TyCoVarSet
fixed_tvs) ])
(TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$ (TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
fixVarSet TyCoVarSet -> TyCoVarSet
extend TyCoVarSet
fixed_tvs
where
extend :: TyCoVarSet -> TyCoVarSet
extend TyCoVarSet
fixed_tvs = (TyCoVarSet -> (TyCoVarSet, TyCoVarSet) -> TyCoVarSet)
-> TyCoVarSet -> [(TyCoVarSet, TyCoVarSet)] -> TyCoVarSet
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' TyCoVarSet -> (TyCoVarSet, TyCoVarSet) -> TyCoVarSet
add TyCoVarSet
fixed_tvs [(TyCoVarSet, TyCoVarSet)]
tv_fds
where
add :: TyCoVarSet -> (TyCoVarSet, TyCoVarSet) -> TyCoVarSet
add TyCoVarSet
fixed_tvs (TyCoVarSet
ls,TyCoVarSet
rs)
| TyCoVarSet
ls TyCoVarSet -> TyCoVarSet -> Bool
`subVarSet` TyCoVarSet
fixed_tvs = TyCoVarSet
fixed_tvs TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` TyCoVarSet -> TyCoVarSet
closeOverKinds TyCoVarSet
rs
| Bool
otherwise = TyCoVarSet
fixed_tvs
tv_fds :: [(TyCoVarSet,TyCoVarSet)]
tv_fds :: [(TyCoVarSet, TyCoVarSet)]
tv_fds = [ ([Type] -> TyCoVarSet
tyCoVarsOfTypes [Type]
ls, FV -> TyCoVarSet
fvVarSet (FV -> TyCoVarSet) -> FV -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$ Bool -> [Type] -> FV
injectiveVarsOfTypes Bool
True [Type]
rs)
| Type
pred <- [Type]
preds
, Type
pred' <- Type
pred Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: Type -> [Type]
transSuperClasses Type
pred
, ([Type]
ls, [Type]
rs) <- Type -> [FunDep Type]
determined Type
pred' ]
determined :: PredType -> [([Type],[Type])]
determined :: Type -> [FunDep Type]
determined Type
pred
= case Type -> Pred
classifyPredType Type
pred of
EqPred EqRel
NomEq Type
t1 Type
t2 -> [([Type
t1],[Type
t2]), ([Type
t2],[Type
t1])]
ClassPred Class
cls [Type]
tys | Bool -> Bool
not (Class -> Bool
isIPClass Class
cls)
-> [ FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
instFD FunDep TyVar
fd [TyVar]
cls_tvs [Type]
tys
| let ([TyVar]
cls_tvs, [FunDep TyVar]
cls_fds) = Class -> ([TyVar], [FunDep TyVar])
classTvsFds Class
cls
, FunDep TyVar
fd <- [FunDep TyVar]
cls_fds ]
Pred
_ -> []
checkFunDeps :: InstEnvs -> ClsInst -> [ClsInst]
checkFunDeps :: InstEnvs -> ClsInst -> [ClsInst]
checkFunDeps InstEnvs
inst_envs (ClsInst { is_tvs :: ClsInst -> [TyVar]
is_tvs = [TyVar]
qtvs1, is_cls :: ClsInst -> Class
is_cls = Class
cls
, is_tys :: ClsInst -> [Type]
is_tys = [Type]
tys1, is_tcs :: ClsInst -> [RoughMatchTc]
is_tcs = [RoughMatchTc]
rough_tcs1 })
| [FunDep TyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FunDep TyVar]
fds
= []
| Bool
otherwise
= (ClsInst -> ClsInst -> Bool) -> [ClsInst] -> [ClsInst]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy ClsInst -> ClsInst -> Bool
eq_inst ([ClsInst] -> [ClsInst]) -> [ClsInst] -> [ClsInst]
forall a b. (a -> b) -> a -> b
$
[ ClsInst
ispec | ClsInst
ispec <- [ClsInst]
cls_insts
, FunDep TyVar
fd <- [FunDep TyVar]
fds
, FunDep TyVar -> ClsInst -> Bool
is_inconsistent FunDep TyVar
fd ClsInst
ispec ]
where
cls_insts :: [ClsInst]
cls_insts = InstEnvs -> Class -> [ClsInst]
classInstances InstEnvs
inst_envs Class
cls
([TyVar]
cls_tvs, [FunDep TyVar]
fds) = Class -> ([TyVar], [FunDep TyVar])
classTvsFds Class
cls
qtv_set1 :: TyCoVarSet
qtv_set1 = [TyVar] -> TyCoVarSet
mkVarSet [TyVar]
qtvs1
is_inconsistent :: FunDep TyVar -> ClsInst -> Bool
is_inconsistent FunDep TyVar
fd (ClsInst { is_tvs :: ClsInst -> [TyVar]
is_tvs = [TyVar]
qtvs2, is_tys :: ClsInst -> [Type]
is_tys = [Type]
tys2, is_tcs :: ClsInst -> [RoughMatchTc]
is_tcs = [RoughMatchTc]
rough_tcs2 })
| [RoughMatchTc] -> [RoughMatchTc] -> Bool
instanceCantMatch [RoughMatchTc]
trimmed_tcs [RoughMatchTc]
rough_tcs2
= Bool
False
| Bool
otherwise
= case BindFun -> [Type] -> [Type] -> Maybe Subst
tcUnifyTyKis BindFun
bind_fn [Type]
ltys1 [Type]
ltys2 of
Maybe Subst
Nothing -> Bool
False
Just Subst
subst
-> Maybe Subst -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe Subst -> Bool) -> Maybe Subst -> Bool
forall a b. (a -> b) -> a -> b
$
BindFun -> [Type] -> [Type] -> Maybe Subst
tcUnifyTyKis BindFun
bind_fn (Subst -> [Type] -> [Type]
substTysUnchecked Subst
subst [Type]
rtys1) (Subst -> [Type] -> [Type]
substTysUnchecked Subst
subst [Type]
rtys2)
where
trimmed_tcs :: [RoughMatchTc]
trimmed_tcs = [TyVar] -> FunDep TyVar -> [RoughMatchTc] -> [RoughMatchTc]
trimRoughMatchTcs [TyVar]
cls_tvs FunDep TyVar
fd [RoughMatchTc]
rough_tcs1
([Type]
ltys1, [Type]
rtys1) = FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
instFD FunDep TyVar
fd [TyVar]
cls_tvs [Type]
tys1
([Type]
ltys2, [Type]
rtys2) = FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
instFD FunDep TyVar
fd [TyVar]
cls_tvs [Type]
tys2
qtv_set2 :: TyCoVarSet
qtv_set2 = [TyVar] -> TyCoVarSet
mkVarSet [TyVar]
qtvs2
bind_fn :: BindFun
bind_fn = TyCoVarSet -> BindFun
matchBindFun (TyCoVarSet
qtv_set1 TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` TyCoVarSet
qtv_set2)
eq_inst :: ClsInst -> ClsInst -> Bool
eq_inst ClsInst
i1 ClsInst
i2 = ClsInst -> TyVar
instanceDFunId ClsInst
i1 TyVar -> TyVar -> Bool
forall a. Eq a => a -> a -> Bool
== ClsInst -> TyVar
instanceDFunId ClsInst
i2
trimRoughMatchTcs :: [TyVar] -> FunDep TyVar -> [RoughMatchTc] -> [RoughMatchTc]
trimRoughMatchTcs :: [TyVar] -> FunDep TyVar -> [RoughMatchTc] -> [RoughMatchTc]
trimRoughMatchTcs [TyVar]
_clas_tvs FunDep TyVar
_ [] = String -> [RoughMatchTc]
forall a. HasCallStack => String -> a
panic String
"trimRoughMatchTcs: nullary [RoughMatchTc]"
trimRoughMatchTcs [TyVar]
clas_tvs ([TyVar]
ltvs, [TyVar]
_) (RoughMatchTc
cls:[RoughMatchTc]
mb_tcs)
= RoughMatchTc
cls RoughMatchTc -> [RoughMatchTc] -> [RoughMatchTc]
forall a. a -> [a] -> [a]
: (TyVar -> RoughMatchTc -> RoughMatchTc)
-> [TyVar] -> [RoughMatchTc] -> [RoughMatchTc]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith TyVar -> RoughMatchTc -> RoughMatchTc
select [TyVar]
clas_tvs [RoughMatchTc]
mb_tcs
where
select :: TyVar -> RoughMatchTc -> RoughMatchTc
select TyVar
clas_tv RoughMatchTc
mb_tc | TyVar
clas_tv TyVar -> [TyVar] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TyVar]
ltvs = RoughMatchTc
mb_tc
| Bool
otherwise = RoughMatchTc
RM_WildCard