%
+% (c) The University of Glasgow 2006
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%
\section[InstEnv]{Utilities for typechecking instance declarations}
InstEnv, emptyInstEnv, extendInstEnv,
extendInstEnvList, lookupInstEnv, instEnvElts,
- classInstances,
+ classInstances, instanceBindFun,
instanceCantMatch, roughMatchTcs
) where
#include "HsVersions.h"
-import Class ( Class )
-import Var ( Id, TyVar, isTcTyVar )
+import Class
+import Var
import VarSet
-import Name ( Name, NamedThing(..), getSrcLoc, nameIsLocalOrFrom, nameModule )
-import OccName ( OccName )
-import NameSet ( unionNameSets, unitNameSet, nameSetToList )
-import Type ( TvSubst )
-import TcType ( Type, PredType, tcEqType,
- tcSplitDFunTy, tyVarsOfTypes, isExistentialTyVar,
- pprThetaArrow, pprClassPred,
- tyClsNamesOfType, tcSplitTyConApp_maybe
- )
-import TyCon ( tyConName )
-import TcGadt ( tcUnifyTys, BindFlag(..) )
-import Unify ( tcMatchTys )
+import Name
+import TcType
+import TyCon
+import Unify
import Outputable
-import BasicTypes ( OverlapFlag(..) )
-import UniqFM ( UniqFM, lookupUFM, emptyUFM, addToUFM_C, eltsUFM )
-import Id ( idType, idName )
-import SrcLoc ( pprDefnLoc )
-import Maybe ( isJust, isNothing )
+import BasicTypes
+import UniqFM
+import Id
+import FastString
+
+import Data.Maybe ( isJust, isNothing )
\end{code}
data Instance
= Instance { is_cls :: Name -- Class name
- -- Used for "rough matching"; see note below
+ -- Used for "rough matching"; see Note [Rough-match field]
+ -- INVARIANT: is_tcs = roughMatchTcs is_tys
, is_tcs :: [Maybe Name] -- Top of type args
- -- Used for "proper matching"; see note
+ -- Used for "proper matching"; see Note [Proper-match fields]
, is_tvs :: TyVarSet -- Template tyvars for full match
, is_tys :: [Type] -- Full arg types
+ -- INVARIANT: is_dfun Id has type
+ -- forall is_tvs. (...) => is_cls is_tys
, is_dfun :: DFunId
, is_flag :: OverlapFlag -- See detailed comments with
-- the decl of BasicTypes.OverlapFlag
-
- , is_orph :: Maybe OccName }
+ }
\end{code}
-The "rough-match" fields
-~~~~~~~~~~~~~~~~~~~~~~~~~
-The is_cls, is_args fields allow a "rough match" to be done
+Note [Rough-match field]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The is_cls, is_tcs fields allow a "rough match" to be done
without poking inside the DFunId. Poking the DFunId forces
us to suck in all the type constructors etc it involves,
which is a total waste of time if it has no chance of matching
different real tycons can't.)
NB: newtypes are not transparent, though!
-The "proper-match" fields
+Note [Proper-match fields]
~~~~~~~~~~~~~~~~~~~~~~~~~
-The is_tvs, is_tys fields are simply cahced values, pulled
+The is_tvs, is_tys fields are simply cached values, pulled
out (lazily) from the dfun id. They are cached here simply so
that we don't need to decompose the DFunId each time we want
to match it. The hope is that the fast-match fields mean
instantiate the dfun's context.)
-Note [Orphans]: the "is_orph" field
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-An instance is an orphan if its head (after the =>) mentions
-nothing defined in this module.
-
- Just n The head mentions n, which is defined in this module
- This is used for versioning; the instance decl is
- considered part of the defn of n when computing versions
-
- Nothing The head mentions nothing defined in this module
-
-If a module contains any orphans, then its interface file is read
-regardless, so that its instances are not missed.
-
-Functional dependencies worsen the situation a bit. Consider
- class C a b | a -> b
-In some other module we might have
- module M where
- data T = ...
- instance C Int T where ...
-This isn't considered an orphan, so we will only read M's interface
-if something from M is used (e.g. T). So there's a risk we'll
-miss the improvement from the instance. Workaround: import M.
-
-Rules are orphans and versioned in much the same way.
\begin{code}
instanceDFunId :: Instance -> DFunId
-- are ok; hence the assert
ispec { is_dfun = dfun, is_tvs = mkVarSet tvs, is_tys = tys }
where
- (tvs, _, _, tys) = tcSplitDFunTy (idType dfun)
+ (tvs, _, tys) = tcSplitDFunTy (idType dfun)
instanceRoughTcs :: Instance -> [Maybe Name]
instanceRoughTcs = is_tcs
pprInstance :: Instance -> SDoc
-- Prints the Instance as an instance declaration
-pprInstance ispec@(Instance { is_flag = flag })
+pprInstance ispec
= hang (pprInstanceHdr ispec)
- 2 (ptext SLIT("--") <+> (pprDefnLoc (getSrcLoc ispec)))
+ 2 (ptext (sLit "--") <+> pprNameLoc (getName ispec))
-- * pprInstanceHdr is used in VStudio to populate the ClassView tree
pprInstanceHdr :: Instance -> SDoc
-- Prints the Instance as an instance declaration
pprInstanceHdr ispec@(Instance { is_flag = flag })
- = ptext SLIT("instance") <+> ppr flag
- <+> sep [pprThetaArrow theta, pprClassPred clas tys]
+ = ptext (sLit "instance") <+> ppr flag
+ <+> sep [pprThetaArrow theta, ppr res_ty]
where
- (_, theta, clas, tys) = instanceHead ispec
+ (_, theta, res_ty) = tcSplitSigmaTy (idType (is_dfun ispec))
-- Print without the for-all, which the programmer doesn't write
pprInstances :: [Instance] -> SDoc
pprInstances ispecs = vcat (map pprInstance ispecs)
-instanceHead :: Instance -> ([TyVar], [PredType], Class, [Type])
-instanceHead ispec = tcSplitDFunTy (idType (is_dfun ispec))
+instanceHead :: Instance -> ([TyVar], ThetaType, Class, [Type])
+instanceHead ispec
+ = (tvs, theta, cls, tys)
+ where
+ (tvs, theta, tau) = tcSplitSigmaTy (idType (is_dfun ispec))
+ (cls, tys) = tcSplitDFunHead tau
mkLocalInstance :: DFunId -> OverlapFlag -> Instance
-- Used for local instances, where we can safely pull on the DFunId
mkLocalInstance dfun oflag
= Instance { is_flag = oflag, is_dfun = dfun,
is_tvs = mkVarSet tvs, is_tys = tys,
- is_cls = cls_name, is_tcs = roughMatchTcs tys,
- is_orph = orph }
+ is_cls = className cls, is_tcs = roughMatchTcs tys }
where
- (tvs, _, cls, tys) = tcSplitDFunTy (idType dfun)
- mod = nameModule (idName dfun)
- cls_name = getName cls
- tycl_names = foldr (unionNameSets . tyClsNamesOfType)
- (unitNameSet cls_name) tys
- orph = case filter (nameIsLocalOrFrom mod) (nameSetToList tycl_names) of
- [] -> Nothing
- (n:ns) -> Just (getOccName n)
-
-mkImportedInstance :: Name -> [Maybe Name] -> Maybe OccName
+ (tvs, cls, tys) = tcSplitDFunTy (idType dfun)
+
+mkImportedInstance :: Name -> [Maybe Name]
-> DFunId -> OverlapFlag -> Instance
-- Used for imported instances, where we get the rough-match stuff
-- from the interface file
-mkImportedInstance cls mb_tcs orph dfun oflag
+mkImportedInstance cls mb_tcs dfun oflag
= Instance { is_flag = oflag, is_dfun = dfun,
is_tvs = mkVarSet tvs, is_tys = tys,
- is_cls = cls, is_tcs = mb_tcs, is_orph = orph }
+ is_cls = cls, is_tcs = mb_tcs }
where
- (tvs, _, _, tys) = tcSplitDFunTy (idType dfun)
+ (tvs, _, tys) = tcSplitDFunTy (idType dfun)
roughMatchTcs :: [Type] -> [Maybe Name]
roughMatchTcs tys = map rough tys
-- possibly be instantiated to actual, nor vice versa;
-- False is non-committal
instanceCantMatch (Just t : ts) (Just a : as) = t/=a || instanceCantMatch ts as
-instanceCantMatch ts as = False -- Safe
+instanceCantMatch _ _ = False -- Safe
\end{code}
add (ClsIE cur_insts cur_tyvar) _ = ClsIE (ins_item : cur_insts)
(ins_tyvar || cur_tyvar)
ins_tyvar = not (any isJust mb_tcs)
-\end{code}
+\end{code}
%************************************************************************
%* *
-\subsection{Looking up an instance}
+ Looking up an instance
%* *
%************************************************************************
thing we are looking up can have an arbitrary "flexi" part.
\begin{code}
-lookupInstEnv :: (InstEnv -- External package inst-env
- ,InstEnv) -- Home-package inst-env
- -> Class -> [Type] -- What we are looking for
- -> ([(TvSubst, Instance)], -- Successful matches
- [Instance]) -- These don't match but do unify
- -- The second component of the tuple happens when we look up
- -- Foo [a]
- -- in an InstEnv that has entries for
- -- Foo [Int]
- -- Foo [b]
- -- Then which we choose would depend on the way in which 'a'
- -- is instantiated. So we report that Foo [b] is a match (mapping b->a)
- -- but Foo [Int] is a unifier. This gives the caller a better chance of
- -- giving a suitable error messagen
+type InstTypes = [Either TyVar Type]
+ -- Right ty => Instantiate with this type
+ -- Left tv => Instantiate with any type of this tyvar's kind
+
+type InstMatch = (Instance, InstTypes)
+\end{code}
+
+Note [InstTypes: instantiating types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A successful match is an Instance, together with the types at which
+ the dfun_id in the Instance should be instantiated
+The instantiating types are (Mabye 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 Nothing indicates that 'b' can be freely instantiated.
+(The caller instantiates it to a flexi type variable, which will presumably
+ presumably later become fixed via functional dependencies.)
+
+\begin{code}
+lookupInstEnv :: (InstEnv, InstEnv) -- External and home package inst-env
+ -> Class -> [Type] -- What we are looking for
+ -> ([InstMatch], -- Successful matches
+ [Instance]) -- These don't match but do unify
+
+-- The second component of the result pair happens when we look up
+-- Foo [a]
+-- in an InstEnv that has entries for
+-- Foo [Int]
+-- Foo [b]
+-- Then which we choose would depend on the way in which 'a'
+-- is instantiated. So we report that Foo [b] is a match (mapping b->a)
+-- but Foo [Int] is a unifier. This gives the caller a better chance of
+-- giving a suitable error messagen
lookupInstEnv (pkg_ie, home_ie) cls tys
= (pruned_matches, all_unifs)
(pkg_matches, pkg_unifs) = lookup pkg_ie
all_matches = home_matches ++ pkg_matches
all_unifs = home_unifs ++ pkg_unifs
- pruned_matches
- | null all_unifs = foldr insert_overlapping [] all_matches
- | otherwise = all_matches -- Non-empty unifs is always an error situation,
- -- so don't attempt to pune the matches
+ pruned_matches = foldr insert_overlapping [] all_matches
+ -- Even if the unifs is non-empty (an error situation)
+ -- we still prune the matches, so that the error message isn't
+ -- misleading (complaining of multiple matches when some should be
+ -- overlapped away)
--------------
lookup env = case lookupUFM env cls of
-> find [] [] insts
--------------
+ lookup_tv :: TvSubst -> TyVar -> Either TyVar Type
+ -- See Note [InstTypes: instantiating types]
+ lookup_tv subst tv = case lookupTyVar subst tv of
+ Just ty -> Right ty
+ Nothing -> Left tv
+
find ms us [] = (ms, us)
find ms us (item@(Instance { is_tcs = mb_tcs, is_tvs = tpl_tvs,
is_tys = tpl_tys, is_flag = oflag,
= find ms us rest
| Just subst <- tcMatchTys tpl_tvs tpl_tys tys
- = find ((subst,item):ms) us rest
+ = let
+ (dfun_tvs, _) = tcSplitForAllTys (idType dfun)
+ in
+ ASSERT( all (`elemVarSet` tpl_tvs) dfun_tvs ) -- Check invariant
+ find ((item, map (lookup_tv subst) dfun_tvs) : ms) us rest
-- Does not match, so next check whether the things unify
-- See Note [overlapping instances] above
)
-- Unification will break badly if the variables overlap
-- They shouldn't because we allocate separate uniques for them
- case tcUnifyTys bind_fn tpl_tys tys of
+ case tcUnifyTys instanceBindFun tpl_tys tys of
Just _ -> find ms (item:us) rest
- Nothing -> find ms us rest
+ Nothing -> find ms us rest
---------------
-bind_fn tv | isTcTyVar tv && isExistentialTyVar tv = Skolem
- | otherwise = BindMe
- -- The key_tys can contain skolem constants, and we can guarantee that those
- -- are never going to be instantiated to anything, so we should not involve
- -- them in the unification test. Example:
- -- class Foo a where { op :: a -> Int }
- -- instance Foo a => Foo [a] -- NB overlap
- -- instance Foo [Int] -- NB overlap
- -- data T = forall a. Foo a => MkT a
- -- f :: T -> Int
- -- f (MkT x) = op [x,x]
- -- The op [x,x] means we need (Foo [a]). Without the filterVarSet we'd
- -- complain, saying that the choice of instance depended on the instantiation
- -- of 'a'; but of course it isn't *going* to be instantiated.
- --
- -- We do this only for pattern-bound skolems. For example we reject
- -- g :: forall a => [a] -> Int
- -- g x = op x
- -- on the grounds that the correct instance depends on the instantiation of 'a'
-
---------------
-insert_overlapping :: (TvSubst, Instance) -> [(TvSubst, Instance)]
- -> [(TvSubst, Instance)]
+insert_overlapping :: InstMatch -> [InstMatch] -> [InstMatch]
-- Add a new solution, knocking out strictly less specific ones
insert_overlapping new_item [] = [new_item]
insert_overlapping new_item (item:items)
new_beats_old = new_item `beats` item
old_beats_new = item `beats` new_item
- (_, instA) `beats` (_, instB)
+ (instA, _) `beats` (instB, _)
= overlap_ok &&
isJust (tcMatchTys (is_tvs instB) (is_tys instB) (is_tys instA))
-- A beats B if A is more specific than B, and B admits overlap
where
overlap_ok = case is_flag instB of
NoOverlap -> False
- other -> True
+ _ -> True
+\end{code}
+
+
+%************************************************************************
+%* *
+ Binding decisions
+%* *
+%************************************************************************
+
+\begin{code}
+instanceBindFun :: TyVar -> BindFlag
+instanceBindFun tv | isTcTyVar tv && isExistentialTyVar tv = Skolem
+ | otherwise = BindMe
+ -- Note [Binding when looking up instances]
\end{code}
+Note [Binding when looking up instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When looking up in the instance environment, or family-instance environment,
+we are careful about multiple matches, as described above in
+Note [Overlapping instances]
+
+The key_tys can contain skolem constants, and we can guarantee that those
+are never going to be instantiated to anything, so we should not involve
+them in the unification test. Example:
+ class Foo a where { op :: a -> Int }
+ instance Foo a => Foo [a] -- NB overlap
+ instance Foo [Int] -- NB overlap
+ data T = forall a. Foo a => MkT a
+ f :: T -> Int
+ f (MkT x) = op [x,x]
+The op [x,x] means we need (Foo [a]). Without the filterVarSet we'd
+complain, saying that the choice of instance depended on the instantiation
+of 'a'; but of course it isn't *going* to be instantiated.
+
+We do this only for pattern-bound skolems. For example we reject
+ g :: forall a => [a] -> Int
+ g x = op x
+on the grounds that the correct instance depends on the instantiation of 'a'
projects / ghc-hetmet.git / blobdiff