Commit 6b0537a1 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Respect kind-variable scoping when instantiating dfuns

Fixes Trac #6020
parent bf6f7085
......@@ -22,9 +22,7 @@ import Unify
import FamInstEnv
import Coercion( mkAxInstRHS )
import Id
import Var
import TcType
import PrelNames (singIClassName)
......@@ -1326,8 +1324,8 @@ instFunDepEqn :: WantedLoc -> Equation -> TcS [(Int,(EvVar,WantedLoc))]
instFunDepEqn wl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
, fd_pred1 = d1, fd_pred2 = d2 })
= do { let tvs = varSetElems qtvs
; tvs' <- mapM instFlexiTcS tvs -- IA0_TODO: we might need to do kind substitution
; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
; tys' <- mapM instFlexiTcS tvs -- IA0_TODO: we might need to do kind substitution
; let subst = zipTopTvSubst tvs tys'
; foldM (do_one subst) [] eqs }
where
do_one subst ievs (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 })
......@@ -1868,14 +1866,11 @@ matchClassInst inerts clas tys loc
MatchInstSingle (dfun_id, mb_inst_tys) ->
do { checkWellStagedDFun pred dfun_id loc
-- It's possible that not all the tyvars are in
-- the substitution, tenv. For example:
-- instance C X a => D X where ...
-- (presumably there's a functional dependency in class C)
-- Hence mb_inst_tys :: Either TyVar TcType
-- mb_inst_tys :: Maybe TcType
-- See Note [DFunInstType: instantiating types] in InstEnv
; tys <- instDFunTypes mb_inst_tys
; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
; (tys, dfun_phi) <- instDFunType dfun_id mb_inst_tys
; let (theta, _) = tcSplitPhiTy dfun_phi
; if null theta then
return (GenInst [] (EvDFunApp dfun_id tys []))
else do
......
......@@ -76,8 +76,7 @@ module TcSMonad (
pprCtTypeMap, partCtFamHeadMap,
instDFunTypes, -- Instantiation
-- instDFunConstraints,
instDFunType, -- Instantiation
newFlexiTcSTy, instFlexiTcS,
compatKind, mkKindErrorCtxtTcS,
......@@ -1245,19 +1244,30 @@ newFlattenSkolemTyVar ty
-- Instantiations
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
instDFunTypes :: [Either TyVar TcType] -> TcS [TcType]
instDFunTypes mb_inst_tys
= mapM inst_tv mb_inst_tys
instDFunType :: DFunId -> [DFunInstType] -> TcS ([TcType], TcType)
instDFunType dfun_id mb_inst_tys
= wrapTcS $ go dfun_tvs mb_inst_tys (mkTopTvSubst [])
where
inst_tv :: Either TyVar TcType -> TcS Type
inst_tv (Left tv) = mkTyVarTy <$> instFlexiTcS tv
inst_tv (Right ty) = return ty
instFlexiTcS :: TyVar -> TcS TcTyVar
(dfun_tvs, dfun_phi) = tcSplitForAllTys (idType dfun_id)
go :: [TyVar] -> [DFunInstType] -> TvSubst -> TcM ([TcType], TcType)
go [] [] subst = return ([], substTy subst dfun_phi)
go (tv:tvs) (Just ty : mb_tys) subst
= do { (tys, phi) <- go tvs mb_tys (extendTvSubst subst tv ty)
; return (ty : tys, phi) }
go (tv:tvs) (Nothing : mb_tys) subst
= do { ty <- instFlexiTcSHelper (tyVarName tv) (substTy subst (tyVarKind tv))
-- Don't forget to instantiate the kind!
-- cf TcMType.tcInstTyVarX
; (tys, phi) <- go tvs mb_tys (extendTvSubst subst tv ty)
; return (ty : tys, phi) }
go _ _ _ = pprPanic "instDFunTypes" (ppr dfun_id $$ ppr mb_inst_tys)
instFlexiTcS :: TyVar -> TcS TcType
-- Like TcM.instMetaTyVar but the variable that is created is
-- always touchable; we are supposed to guess its instantiation.
-- See Note [Touchable meta type variables]
instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv)
instFlexiTcS tv = wrapTcS (instFlexiTcSHelper (tyVarName tv) (tyVarKind tv) )
newFlexiTcSTy :: Kind -> TcS TcType
newFlexiTcSTy knd
......@@ -1273,14 +1283,13 @@ isFlexiTcsTv tv
| MetaTv TcsTv _ <- tcTyVarDetails tv = True
| otherwise = False
instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
instFlexiTcSHelper :: Name -> Kind -> TcM TcType
instFlexiTcSHelper tvname tvkind
= wrapTcS $
do { uniq <- TcM.newUnique
= do { uniq <- TcM.newUnique
; ref <- TcM.newMutVar Flexi
; let name = setNameUnique tvname uniq
kind = tvkind
; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
; return (mkTyVarTy (mkTcTyVar name kind (MetaTv TcsTv ref))) }
-- Creating and setting evidence variables and CtFlavors
......@@ -1361,8 +1370,7 @@ newDerived pty
newKindConstraint :: TcTyVar -> Kind -> TcS (MaybeNew EvVar)
-- Create new wanted CoVar that constrains the type to have the specified kind.
newKindConstraint tv knd
= do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd
; let ty_k = mkTyVarTy tv_k
= do { ty_k <- wrapTcS (instFlexiTcSHelper (tyVarName tv) knd)
; newWantedEvVar (mkTcEqPred (mkTyVarTy tv) ty_k) }
instDFunConstraints :: TcThetaType -> TcS [MaybeNew EvVar]
......@@ -1476,7 +1484,7 @@ data MatchInstResult mi
| MatchInstMany -- Multiple matching instances
matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType]))
matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Maybe TcType]))
-- Look up a class constraint in the instance environment
matchClass clas tys
= do { let pred = mkClassPred clas tys
......
......@@ -9,7 +9,7 @@ The bits common to TcInstDcls and TcDeriv.
\begin{code}
module InstEnv (
DFunId, OverlapFlag(..), InstMatch, ClsInstLookupResult,
ClsInst(..), pprInstance, pprInstanceHdr, pprInstances,
ClsInst(..), DFunInstType, pprInstance, pprInstanceHdr, pprInstances,
instanceHead, mkLocalInstance, mkImportedInstance,
instanceDFunId, setInstanceDFunId, instanceRoughTcs,
......@@ -428,11 +428,12 @@ the env is kept ordered, the first match must be the only one. The
thing we are looking up can have an arbitrary "flexi" part.
\begin{code}
type InstTypes = [Either TyVar Type]
-- Right ty => Instantiate with this type
-- Left tv => Instantiate with any type of this tyvar's kind
type DFunInstType = Maybe Type
-- Just ty => Instantiate with this type
-- Nothing => Instantiate with any type of this tyvar's kind
-- See Note [DFunInstType: instantiating types]
type InstMatch = (ClsInst, InstTypes)
type InstMatch = (ClsInst, [DFunInstType])
type ClsInstLookupResult
= ( [InstMatch] -- Successful matches
......@@ -441,16 +442,16 @@ type ClsInstLookupResult
-- SafeHaskell condition.
\end{code}
Note [InstTypes: instantiating types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Note [DFunInstType: instantiating types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A successful match is an ClsInst, together with the types at which
the dfun_id in the ClsInst should be instantiated
The instantiating types are (Either TyVar Type)s because the dfun
might have some tyvars that *only* appear in arguments
dfun :: forall a b. C a b, Ord b => D [a]
When we match this against D [ty], we return the instantiating types
[Right ty, Left b]
where the 'Left b' indicates that 'b' can be freely instantiated.
[Just ty, Nothing]
where the 'Nothing' indicates that 'b' can be freely instantiated.
(The caller instantiates it to a flexi type variable, which will
presumably later become fixed via functional dependencies.)
......@@ -469,12 +470,9 @@ lookupUniqueInstEnv instEnv cls tys
| otherwise -> Left $ ptext (sLit "flexible type variable:") <+>
(ppr $ mkTyConApp (classTyCon cls) tys)
where
inst_tys' = [ty | Right ty <- inst_tys]
noFlexiVar = all isRight inst_tys
inst_tys' = [ty | Just ty <- inst_tys]
noFlexiVar = all isJust inst_tys
_other -> Left $ ptext (sLit "instance not found") <+> (ppr $ mkTyConApp (classTyCon cls) tys)
where
isRight (Left _) = False
isRight (Right _) = True
lookupInstEnv' :: InstEnv -- InstEnv to look in
-> Class -> [Type] -- What we are looking for
......@@ -533,11 +531,11 @@ lookupInstEnv' ie cls tys
Nothing -> find ms us rest
----------------
lookup_tv :: TvSubst -> TyVar -> Either TyVar Type
-- See Note [InstTypes: instantiating types]
lookup_tv :: TvSubst -> TyVar -> DFunInstType
-- See Note [DFunInstType: instantiating types]
lookup_tv subst tv = case lookupTyVar subst tv of
Just ty -> Right ty
Nothing -> Left tv
Just ty -> Just ty
Nothing -> Nothing
---------------
-- This is the common way to call this function.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment