%
+% (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 Unify ( tcMatchTys, tcUnifyTys, BindFlag(..) )
+import Name
+import TcType
+import TyCon
+import Unify
import Outputable
-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}
%************************************************************************
\begin{code}
-type DFunId = Id
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 -- See Note [Haddock assumptions]
+ , is_flag :: OverlapFlag -- See detailed comments with
+ -- the decl of BasicTypes.OverlapFlag
+ }
+\end{code}
- , is_dfun :: DFunId
- , is_flag :: OverlapFlag
-
- , is_orph :: Maybe OccName }
-
--- The "rough-match" fields
--- ~~~~~~~~~~~~~~~~~~~~~~~~~
--- The is_cls, is_args 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
--- So the Name, [Maybe Name] fields allow us to say "definitely
--- does not match", based only on the Name.
---
--- In is_tcs,
--- Nothing means that this type arg is a type variable
---
--- (Just n) means that this type arg is a
--- TyConApp with a type constructor of n.
--- This is always a real tycon, never a synonym!
--- (Two different synonyms might match, but two
--- different real tycons can't.)
--- NB: newtypes are not transparent, though!
---
--- The "proper-match" fields
--- ~~~~~~~~~~~~~~~~~~~~~~~~~
--- The is_tvs, is_tys fields are simply cahced 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
--- that we often never poke th proper-match fields
---
--- However, note that:
--- * is_tvs must be a superset of the free vars of is_tys
---
--- * The is_dfun must itself be quantified over exactly is_tvs
--- (This is so that we can use the matching substitution to
--- instantiate the dfun's context.)
---
--- The "orphan" 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.
+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
+So the Name, [Maybe Name] fields allow us to say "definitely
+does not match", based only on the Name.
+
+In is_tcs,
+ Nothing means that this type arg is a type variable
+
+ (Just n) means that this type arg is a
+ TyConApp with a type constructor of n.
+ This is always a real tycon, never a synonym!
+ (Two different synonyms might match, but two
+ different real tycons can't.)
+ NB: newtypes are not transparent, though!
+
+Note [Proper-match fields]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+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
+that we often never poke th proper-match fields
+
+However, note that:
+ * is_tvs must be a superset of the free vars of is_tys
+
+ * The is_dfun must itself be quantified over exactly is_tvs
+ (This is so that we can use the matching substitution to
+ instantiate the dfun's context.)
+
+Note [Haddock assumptions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+For normal user-written instances, Haddock relies on
+
+ * the SrcSpan of
+ * the Name of
+ * the is_dfun of
+ * an Instance
+
+being equal to
+
+ * the SrcSpan of
+ * the instance head type of
+ * the InstDecl used to construct the Instance.
+\begin{code}
instanceDFunId :: Instance -> DFunId
instanceDFunId = is_dfun
setInstanceDFunId :: Instance -> DFunId -> Instance
setInstanceDFunId ispec dfun
- = ASSERT( idType dfun `tcEqType` idType (is_dfun ispec) )
+ = ASSERT( idType dfun `eqType` idType (is_dfun ispec) )
-- We need to create the cached fields afresh from
-- the new dfun id. In particular, the is_tvs in
-- the Instance must match those in the dfun!
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]
+ = getPprStyle $ \ sty ->
+ let theta_to_print
+ | debugStyle sty = theta
+ | otherwise = drop (dfunNSilent dfun) theta
+ in ptext (sLit "instance") <+> ppr flag
+ <+> sep [pprThetaArrowTy theta_to_print, ppr res_ty]
where
- (_, theta, clas, tys) = instanceHead ispec
+ dfun = is_dfun ispec
+ (_, theta, res_ty) = tcSplitSigmaTy (idType dfun)
-- 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))
-
-mkLocalInstance :: DFunId -> OverlapFlag -> Instance
+instanceHead :: Instance -> ([TyVar], ThetaType, Class, [Type])
+-- Returns the *source* theta, without the silent arguments
+instanceHead ispec
+ = (tvs, drop n_silent theta, cls, tys)
+ where
+ (tvs, theta, tau) = tcSplitSigmaTy (idType dfun)
+ (cls, tys) = tcSplitDFunHead tau
+ dfun = is_dfun ispec
+ n_silent = dfunNSilent dfun
+
+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
+
+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)
-- 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
-
----------------------------------------------------
-data OverlapFlag
- = NoOverlap -- This instance must not overlap another
-
- | OverlapOk -- Silently ignore this instance if you find a
- -- more specific one that matches the constraint
- -- you are trying to resolve
- --
- -- Example: constraint (Foo [Int])
- -- instances (Foo [Int])
- -- (Foo [a]) OverlapOk
- -- Since the second instance has the OverlapOk flag,
- -- the first instance will be chosen (otherwise
- -- its ambiguous which to choose)
-
- | Incoherent -- Like OverlapOk, but also ignore this instance
- -- if it doesn't match the constraint you are
- -- trying to resolve, but could match if the type variables
- -- in the constraint were instantiated
- --
- -- Example: constraint (Foo [b])
- -- instances (Foo [Int]) Incoherent
- -- (Foo [a])
- -- Without the Incoherent flag, we'd complain that
- -- instantiating 'b' would change which instance
- -- was chosen
- deriving( Eq )
-
-instance Outputable OverlapFlag where
- ppr NoOverlap = empty
- ppr OverlapOk = ptext SLIT("[overlap ok]")
- ppr Incoherent = ptext SLIT("[incoherent]")
+instanceCantMatch _ _ = False -- Safe
\end{code}
-- If *not* then the common case of looking up
-- (C a b c) can fail immediately
+instance Outputable ClsInstEnv where
+ ppr (ClsIE is b) = ptext (sLit "ClsIE") <+> ppr b <+> pprInstances is
+
-- INVARIANTS:
-- * The is_tvs are distinct in each Instance
-- of a ClsInstEnv (so we can safely unify them)
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
+ -- See Note [Overlapping instances] above
| Incoherent <- oflag
= find ms us rest
| otherwise
- = ASSERT2( not (tyVarsOfTypes tys `intersectsVarSet` tpl_tvs),
- (ppr cls <+> ppr tys <+> ppr all_tvs) $$
- (ppr dfun <+> ppr tpl_tvs <+> ppr tpl_tys)
+ = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
+ (ppr cls <+> ppr tys <+> ppr all_tvs) $$
+ (ppr dfun <+> ppr tpl_tvs <+> ppr tpl_tys)
)
-- 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)
- = 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
- -- I.e. if B can be instantiated to match A
- where
- overlap_ok = case is_flag instB of
- NoOverlap -> False
- other -> True
+ (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,
+ -- (ie. if B can be instantiated to match A)
+ -- and overlap is permitted
+ where
+ -- Overlap permitted if *either* instance permits overlap
+ -- This is a change (Trac #3877, Dec 10). It used to
+ -- require that instB (the less specific one) permitted overlap.
+ overlap_ok = case (is_flag instA, is_flag instB) of
+ (NoOverlap, NoOverlap) -> False
+ _ -> True
+\end{code}
+
+
+%************************************************************************
+%* *
+ Binding decisions
+%* *
+%************************************************************************
+
+\begin{code}
+instanceBindFun :: TyVar -> BindFlag
+instanceBindFun tv | isTcTyVar tv && isOverlappableTyVar 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 isOverlappableTyVar 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'