{-# LANGUAGE DeriveFunctor #-}
module GHC.Tc.Instance.FunDeps
( FunDepEqn(..)
, pprEquation
, improveFromInstEnv
, improveFromAnother
, checkInstCoverage
, checkFunDeps
, pprFundeps
, instFD, closeWrtFunDeps
)
where
import GHC.Prelude
import GHC.Types.Name
import GHC.Types.Var
import GHC.Core.Class
import GHC.Core.Predicate
import GHC.Core.Type
import GHC.Tc.Utils.TcType( transSuperClasses )
import GHC.Core.Coercion.Axiom( TypeEqn )
import GHC.Core.Unify
import GHC.Core.InstEnv
import GHC.Types.Var.Set
import GHC.Types.Var.Env
import GHC.Core.TyCo.FVs
import GHC.Core.TyCo.Ppr( pprWithExplicitKindsWhen )
import GHC.Types.SrcLoc
import GHC.Utils.Outputable
import GHC.Utils.FV
import GHC.Utils.Error( Validity'(..), Validity, allValid )
import GHC.Utils.Misc
import GHC.Utils.Panic
import GHC.Data.Pair ( Pair(..) )
import Data.List ( nubBy )
import Data.Maybe
import Data.Foldable ( fold )
data FunDepEqn loc
= FDEqn { forall loc. FunDepEqn loc -> [TyVar]
fd_qtvs :: [TyVar]
, forall loc. FunDepEqn loc -> [TypeEqn]
fd_eqs :: [TypeEqn]
, forall loc. FunDepEqn loc -> Type
fd_pred1 :: PredType
, forall loc. FunDepEqn loc -> Type
fd_pred2 :: PredType
, 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
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_pred1 :: Type
fd_pred1 = Type
pred1, fd_pred2 :: Type
fd_pred2 = Type
pred2, 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 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
_ = []
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
vcat [String -> SDoc
text String
"forall" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
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
vcat [ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
t1 SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"~" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
t2
| Pair Type
t1 Type
t2 <- [TypeEqn]
pairs])]
improveFromInstEnv :: InstEnvs
-> (PredType -> SrcSpan -> loc)
-> Class -> [Type]
-> [FunDepEqn loc]
improveFromInstEnv :: forall loc.
InstEnvs
-> (Type -> SrcSpan -> loc) -> Class -> [Type] -> [FunDepEqn loc]
improveFromInstEnv InstEnvs
inst_env Type -> SrcSpan -> loc
mk_loc Class
cls [Type]
tys
= [ FDEqn { fd_qtvs :: [TyVar]
fd_qtvs = [TyVar]
meta_tvs, fd_eqs :: [TypeEqn]
fd_eqs = [TypeEqn]
eqs
, fd_pred1 :: Type
fd_pred1 = Type
p_inst, fd_pred2 :: Type
fd_pred2 = Type
pred
, fd_loc :: loc
fd_loc = Type -> SrcSpan -> loc
mk_loc Type
p_inst (TyVar -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan (ClsInst -> TyVar
is_dfun 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
, let p_inst :: Type
p_inst = Class -> [Type] -> Type
mkClassPred Class
cls (ClsInst -> [Type]
is_tys ClsInst
ispec)
]
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
pred :: Type
pred = Class -> [Type] -> Type
mkClassPred Class
cls [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
<+> [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 [Type] -> [Type] -> Maybe TCvSubst
tcMatchTyKis [Type]
ltys1 [Type]
ltys2 of
Maybe TCvSubst
Nothing -> []
Just TCvSubst
subst | Maybe TCvSubst -> Bool
forall a. Maybe a -> Bool
isJust (TCvSubst -> [Type] -> [Type] -> Maybe TCvSubst
tcMatchTyKisX TCvSubst
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 (TCvSubst -> Type -> Type
substTyUnchecked TCvSubst
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 (TCvSubst -> Type -> Type
substTyUnchecked TCvSubst
subst (TyVar -> Type
varType TyVar
tv))
| TyVar
tv <- [TyVar]
qtvs, TyVar
tv TyVar -> TCvSubst -> Bool
`notElemTCvSubst` TCvSubst
subst ]
where
([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
checkInstCoverage :: Bool
-> Class -> [PredType] -> [Type]
-> Validity
checkInstCoverage :: Bool -> Class -> [Type] -> [Type] -> Validity
checkInstCoverage Bool
be_liberal Class
clas [Type]
theta [Type]
inst_taus
= [Validity] -> Validity
forall a. [Validity' a] -> Validity' a
allValid ((FunDep TyVar -> Validity) -> [FunDep TyVar] -> [Validity]
forall a b. (a -> b) -> [a] -> [b]
map FunDep TyVar -> Validity
fundep_ok [FunDep TyVar]
fds)
where
([TyVar]
tyvars, [FunDep TyVar]
fds) = Class -> ([TyVar], [FunDep TyVar])
classTvsFds Class
clas
fundep_ok :: FunDep TyVar -> Validity
fundep_ok FunDep TyVar
fd
| Pair Bool -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and (TyCoVarSet -> Bool
isEmptyVarSet (TyCoVarSet -> Bool) -> Pair TyCoVarSet -> Pair Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair TyCoVarSet
undetermined_tvs) = Validity
forall a. Validity' a
IsValid
| Bool
otherwise = SDoc -> Validity
forall a. a -> Validity' a
NotValid SDoc
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
splitVisVarsOfTypes [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
undet_set :: TyCoVarSet
undet_set = Pair TyCoVarSet -> TyCoVarSet
forall m. Monoid m => Pair m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Pair TyCoVarSet
undetermined_tvs
msg :: SDoc
msg = Bool -> SDoc -> SDoc
pprWithExplicitKindsWhen
(TyCoVarSet -> Bool
isEmptyVarSet (TyCoVarSet -> Bool) -> TyCoVarSet -> Bool
forall a b. (a -> b) -> a -> b
$ Pair TyCoVarSet -> TyCoVarSet
forall a. Pair a -> a
pSnd Pair TyCoVarSet
undetermined_tvs) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [
[SDoc] -> SDoc
sep [ String -> SDoc
text String
"The"
SDoc -> SDoc -> SDoc
<+> Bool -> SDoc -> SDoc
ppWhen Bool
be_liberal (String -> SDoc
text String
"liberal")
SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"coverage condition fails in class"
SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Class -> SDoc
forall a. Outputable a => a -> SDoc
ppr Class
clas)
, Int -> SDoc -> SDoc
nest Int
2 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"for functional dependency:"
SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (FunDep TyVar -> SDoc
forall a. Outputable a => FunDep a -> SDoc
pprFunDep FunDep TyVar
fd) ]
, [SDoc] -> SDoc
sep [ String -> SDoc
text String
"Reason: lhs type"SDoc -> SDoc -> SDoc
<>[Type] -> SDoc
forall a. [a] -> SDoc
plural [Type]
ls SDoc -> SDoc -> SDoc
<+> [Type] -> SDoc
forall a. Outputable a => [a] -> SDoc
pprQuotedList [Type]
ls
, Int -> SDoc -> SDoc
nest Int
2 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
(if [Type] -> Bool
forall a. [a] -> Bool
isSingleton [Type]
ls
then String -> SDoc
text String
"does not"
else String -> SDoc
text String
"do not jointly")
SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"determine rhs type"SDoc -> SDoc -> SDoc
<>[Type] -> SDoc
forall a. [a] -> SDoc
plural [Type]
rs
SDoc -> SDoc -> SDoc
<+> [Type] -> SDoc
forall a. Outputable a => [a] -> SDoc
pprQuotedList [Type]
rs ]
, String -> SDoc
text String
"Un-determined variable" SDoc -> SDoc -> SDoc
<> TyCoVarSet -> SDoc
pluralVarSet TyCoVarSet
undet_set SDoc -> SDoc -> SDoc
<> SDoc
colon
SDoc -> SDoc -> SDoc
<+> TyCoVarSet -> ([TyVar] -> SDoc) -> SDoc
pprVarSet TyCoVarSet
undet_set ((TyVar -> SDoc) -> [TyVar] -> SDoc
forall a. (a -> SDoc) -> [a] -> SDoc
pprWithCommas TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr)
, Bool -> SDoc -> SDoc
ppWhen (Bool -> Bool
not Bool
be_liberal Bool -> Bool -> Bool
&&
Pair Bool -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and (TyCoVarSet -> Bool
isEmptyVarSet (TyCoVarSet -> Bool) -> Pair TyCoVarSet -> Pair Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair TyCoVarSet
liberal_undet_tvs)) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
String -> SDoc
text String
"Using UndecidableInstances might help" ]
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
vcat [ String -> SDoc
text String
"closeWrtFunDeps: fixed_tvs is not closed over kinds"
, String -> SDoc
text String
"fixed_tvs:" SDoc -> SDoc -> SDoc
<+> TyCoVarSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCoVarSet
fixed_tvs
, String -> SDoc
text String
"closure:" SDoc -> SDoc -> SDoc
<+> 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 -> [ 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 TCvSubst
tcUnifyTyKis BindFun
bind_fn [Type]
ltys1 [Type]
ltys2 of
Maybe TCvSubst
Nothing -> Bool
False
Just TCvSubst
subst
-> Maybe TCvSubst -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe TCvSubst -> Bool) -> Maybe TCvSubst -> Bool
forall a b. (a -> b) -> a -> b
$
BindFun -> [Type] -> [Type] -> Maybe TCvSubst
tcUnifyTyKis BindFun
bind_fn (TCvSubst -> [Type] -> [Type]
substTysUnchecked TCvSubst
subst [Type]
rtys1) (TCvSubst -> [Type] -> [Type]
substTysUnchecked TCvSubst
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. 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