[project @ 1999-05-18 15:03:54 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / Inst.lhs
index fd24281..155ed13 100644 (file)
@@ -1,68 +1,83 @@
 %
-% (c) The GRASP/AQUA Project, Glasgow University, 1992-1996
+% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
 \section[Inst]{The @Inst@ type: dictionaries or method instances}
 
 \begin{code}
-#include "HsVersions.h"
-
 module Inst (
-       Inst(..),       -- Visible only to TcSimplify
+       LIE, emptyLIE, unitLIE, plusLIE, consLIE, zonkLIE,
+       plusLIEs, mkLIE, isEmptyLIE,
 
-       InstOrigin(..), OverloadedLit(..),
-       LIE(..), emptyLIE, unitLIE, plusLIE, consLIE, zonkLIE, plusLIEs,
+       Inst, OverloadedLit(..),
+       pprInst, pprInsts, pprInstsInFull, tidyInst, tidyInsts,
 
-        InstanceMapper(..),
+        InstanceMapper,
 
-       newDicts, newDictsAtLoc, newMethod, newMethodWithGivenTy, newOverloadedLit,
+       newDictFromOld, newDicts, newDictsAtLoc, 
+       newMethod, newMethodWithGivenTy, newOverloadedLit, instOverloadedFun,
 
-       instType, tyVarsOfInst, lookupInst,
+       tyVarsOfInst, instLoc, getDictClassTys,
 
-       isDict, isTyVarDict, 
+       lookupInst, lookupSimpleInst, LookupInstResult(..),
 
-       zonkInst, instToId,
+       isDict, isTyVarDict, isStdClassTyVarDict, isMethodFor,
+       instBindingRequired, instCanBeGeneralised,
 
-       matchesInst,
-       instBindingRequired, instCanBeGeneralised
+       zonkInst, instToId, instToIdBndr,
 
+       InstOrigin(..), pprOrigin
     ) where
 
-import Ubiq
-
-import HsSyn   ( HsLit(..), HsExpr(..), HsBinds, 
-                 InPat, OutPat, Stmt, Qual, Match,
-                 ArithSeqInfo, PolyType, Fake )
-import RnHsSyn ( RenamedArithSeqInfo(..), RenamedHsExpr(..) )
-import TcHsSyn ( TcIdOcc(..), TcExpr(..), TcIdBndr(..),
-                 mkHsTyApp, mkHsDictApp )
+#include "HsVersions.h"
 
+import HsSyn   ( HsLit(..), HsExpr(..) )
+import RnHsSyn ( RenamedArithSeqInfo, RenamedHsExpr, RenamedPat )
+import TcHsSyn ( TcExpr, TcId, 
+                 mkHsTyApp, mkHsDictApp, zonkId
+               )
 import TcMonad
-import TcEnv   ( tcLookupGlobalValueByKey )
-import TcType  ( TcType(..), TcRhoType(..), TcMaybe, TcTyVarSet(..),
-                 tcInstType, tcInstTcType, zonkTcType )
-
-import Bag     ( emptyBag, unitBag, unionBags, unionManyBags, listToBag, consBag )
-import Class   ( Class(..), GenClass, ClassInstEnv(..), getClassInstEnv )
-import Id      ( GenId, idType, mkInstId )
-import MatchEnv        ( lookupMEnv, insertMEnv )
-import Name    ( mkLocalName, getLocalName, Name )
+import TcEnv   ( TcIdSet, tcLookupValueByKey, tcLookupTyConByKey )
+import TcType  ( TcThetaType,
+                 TcType, TcTauType, TcTyVarSet,
+                 zonkTcType, zonkTcTypes, 
+                 zonkTcThetaType
+               )
+import Bag
+import Class   ( classInstEnv, Class )
+import Id      ( Id, idFreeTyVars, idType, mkUserLocal, mkSysLocal )
+import VarSet  ( elemVarSet )
+import PrelInfo        ( isStandardClass, isCcallishClass, isNoDictClass )
+import Name    ( OccName, Name, mkDictOcc, mkMethodOcc, getOccName )
+import PprType ( pprConstraint )       
+import InstEnv ( InstEnv, lookupInstEnv )
+import SrcLoc  ( SrcLoc )
+import Type    ( Type, ThetaType,
+                 mkTyVarTy, isTyVarTy, mkDictTy, splitForAllTys, splitSigmaTy,
+                 splitRhoTy, tyVarsOfType, tyVarsOfTypes,
+                 mkSynTy, tidyOpenType, tidyOpenTypes
+               )
+import InstEnv ( InstEnv )
+import Subst   ( emptyInScopeSet, mkSubst,
+                 substTy, substTheta, mkTyVarSubst, mkTopTyVarSubst
+               )
+import TyCon   ( TyCon )
+import Subst   ( mkTyVarSubst )
+import VarEnv  ( lookupVarEnv, TidyEnv,
+                 lookupSubstEnv, SubstResult(..)
+               )
+import VarSet  ( unionVarSet )
+import TysPrim   ( intPrimTy, floatPrimTy, doublePrimTy )
+import TysWiredIn ( intDataCon, isIntTy, inIntRange,
+                   floatDataCon, isFloatTy,
+                   doubleDataCon, isDoubleTy,
+                   integerTy, isIntegerTy
+                 ) 
+import Unique  ( fromRationalClassOpKey, rationalTyConKey,
+                 fromIntClassOpKey, fromIntegerClassOpKey, Unique
+               )
+import Maybes  ( expectJust )
+import Util    ( thenCmp, zipWithEqual, mapAccumL )
 import Outputable
-import PprType ( GenClass, TyCon, GenType, GenTyVar )  
-import PprStyle        ( PprStyle(..) )
-import Pretty
-import RnHsSyn ( RnName{-instance NamedThing-} )
-import SpecEnv ( SpecEnv(..) )
-import SrcLoc  ( SrcLoc, mkUnknownSrcLoc )
-import Type    ( GenType, eqSimpleTy,
-                 isTyVarTy, mkDictTy, splitForAllTy, splitSigmaTy,
-                 splitRhoTy, matchTy, tyVarsOfType, tyVarsOfTypes )
-import TyVar   ( GenTyVar )
-import TysPrim   ( intPrimTy )
-import TysWiredIn ( intDataCon )
-import Unique  ( Unique, showUnique,
-                 fromRationalClassOpKey, fromIntClassOpKey, fromIntegerClassOpKey )
-import Util    ( panic, zipEqual, zipWithEqual, assoc, assertPanic )
-
 \end{code}
 
 %************************************************************************
@@ -72,16 +87,27 @@ import Util ( panic, zipEqual, zipWithEqual, assoc, assertPanic )
 %************************************************************************
 
 \begin{code}
-type LIE s = Bag (Inst s)
+type LIE = Bag Inst
 
+isEmptyLIE       = isEmptyBag
 emptyLIE          = emptyBag
 unitLIE inst     = unitBag inst
+mkLIE insts      = listToBag insts
 plusLIE lie1 lie2 = lie1 `unionBags` lie2
 consLIE inst lie  = inst `consBag` lie
 plusLIEs lies    = unionManyBags lies
 
-zonkLIE :: LIE s -> NF_TcM s (LIE s)
+zonkLIE :: LIE -> NF_TcM s LIE
 zonkLIE lie = mapBagNF_Tc zonkInst lie
+
+pprInsts :: [Inst] -> SDoc
+pprInsts insts = parens (sep (punctuate comma (map pprInst insts)))
+
+
+pprInstsInFull insts
+  = vcat (map go insts)
+  where
+    go inst = quotes (ppr inst) <+> pprOrigin inst
 \end{code}
 
 %************************************************************************
@@ -99,238 +125,298 @@ type Int, represented by
        Method 34 doubleId [Int] origin
 
 \begin{code}
-data Inst s
+data Inst
   = Dict
        Unique
-       Class           -- The type of the dict is (c t), where
-       (TcType s)      -- c is the class and t the type;
-       (InstOrigin s)
+       Class           -- The type of the dict is (c ts), where
+       [TcType]        -- c is the class and ts the types;
+       InstOrigin
        SrcLoc
 
   | Method
        Unique
 
-       (TcIdOcc s)     -- The overloaded function
+       TcId    -- The overloaded function
                        -- This function will be a global, local, or ClassOpId;
                        --   inside instance decls (only) it can also be an InstId!
                        -- The id needn't be completely polymorphic.
                        -- You'll probably find its name (for documentation purposes)
                        --        inside the InstOrigin
 
-       [TcType s]      -- The types to which its polymorphic tyvars
+       [TcType]        -- The types to which its polymorphic tyvars
                        --      should be instantiated.
                        -- These types must saturate the Id's foralls.
 
-       (TcRhoType s)   -- Cached: (type-of-id applied to inst_tys)
-                       -- If this type is (theta => tau) then the type of the Method
-                       -- is tau, and the method can be built by saying 
-                       --      id inst_tys dicts
-                       -- where dicts are constructed from theta
+       TcThetaType     -- The (types of the) dictionaries to which the function
+                       -- must be applied to get the method
+
+       TcTauType       -- The type of the method
 
-       (InstOrigin s)
+       InstOrigin
        SrcLoc
 
+       -- INVARIANT: in (Method u f tys theta tau loc)
+       --      type of (f tys dicts(from theta)) = tau
+
   | LitInst
        Unique
        OverloadedLit
-       (TcType s)      -- The type at which the literal is used
-       (InstOrigin s)  -- Always a literal; but more convenient to carry this around
+       TcType          -- The type at which the literal is used
+       InstOrigin      -- Always a literal; but more convenient to carry this around
        SrcLoc
 
 data OverloadedLit
   = OverloadedIntegral  Integer        -- The number
   | OverloadedFractional Rational      -- The number
-
-getInstOrigin (Dict   u clas ty     origin loc) = origin
-getInstOrigin (Method u clas ty rho origin loc) = origin
-getInstOrigin (LitInst u lit ty     origin loc) = origin
 \end{code}
 
-Construction
-~~~~~~~~~~~~
+Ordering
+~~~~~~~~
+@Insts@ are ordered by their class/type info, rather than by their
+unique.  This allows the context-reduction mechanism to use standard finite
+maps to do their stuff.
 
 \begin{code}
-newDicts :: InstOrigin s
-        -> [(Class, TcType s)]
-        -> NF_TcM s (LIE s, [TcIdOcc s])
-newDicts orig theta
- = tcGetSrcLoc                         `thenNF_Tc` \ loc ->
-   tcGetUniques (length theta)         `thenNF_Tc` \ new_uniqs ->
-   let
-       mk_dict u (clas, ty) = Dict u clas ty orig loc
-       dicts = zipWithEqual mk_dict new_uniqs theta
-   in
-   returnNF_Tc (listToBag dicts, map instToId dicts)
-
-newDictsAtLoc orig loc theta   -- Local function, similar to newDicts, 
-                               -- but with slightly different interface
- = tcGetUniques (length theta)         `thenNF_Tc` \ new_uniqs ->
-   let
-       mk_dict u (clas, ty) = Dict u clas ty orig loc
-       dicts = zipWithEqual mk_dict new_uniqs theta
-   in
-   returnNF_Tc (dicts, map instToId dicts)
-
-newMethod :: InstOrigin s
-         -> TcIdOcc s
-         -> [TcType s]
-         -> NF_TcM s (LIE s, TcIdOcc s)
-newMethod orig id tys
- =     -- Get the Id type and instantiate it at the specified types
-   (case id of
-       RealId id -> let (tyvars, rho) = splitForAllTy (idType id)
-                    in tcInstType (tyvars `zipEqual` tys) rho
-       TcId   id -> let (tyvars, rho) = splitForAllTy (idType id)
-                    in tcInstTcType (tyvars `zipEqual` tys) rho
-   )                                           `thenNF_Tc` \ rho_ty ->
-
-       -- Our friend does the rest
-   newMethodWithGivenTy orig id tys rho_ty
-
-
-newMethodWithGivenTy orig id tys rho_ty
- = tcGetSrcLoc                 `thenNF_Tc` \ loc ->
-   tcGetUnique                         `thenNF_Tc` \ new_uniq ->
-   let
-       meth_inst = Method new_uniq id tys rho_ty orig loc
-   in
-   returnNF_Tc (unitLIE meth_inst, instToId meth_inst)
-
-newMethodAtLoc :: InstOrigin s -> SrcLoc -> Id -> [TcType s] -> NF_TcM s (Inst s, TcIdOcc s)
-newMethodAtLoc orig loc real_id tys    -- Local function, similar to newMethod but with 
-                                       -- slightly different interface
- =     -- Get the Id type and instantiate it at the specified types
-   let
-       (tyvars,rho) = splitForAllTy (idType real_id)
-   in
-   tcInstType (tyvars `zipEqual` tys) rho      `thenNF_Tc` \ rho_ty ->
-   tcGetUnique                                         `thenNF_Tc` \ new_uniq ->
-   let
-       meth_inst = Method new_uniq (RealId real_id) tys rho_ty orig loc
-   in
-   returnNF_Tc (meth_inst, instToId meth_inst)
-
-newOverloadedLit :: InstOrigin s
-                -> OverloadedLit
-                -> TcType s
-                -> NF_TcM s (LIE s, TcIdOcc s)
-newOverloadedLit orig lit ty
- = tcGetSrcLoc                 `thenNF_Tc` \ loc ->
-   tcGetUnique                         `thenNF_Tc` \ new_uniq ->
-   let
-       lit_inst = LitInst new_uniq lit ty orig loc
-   in
-   returnNF_Tc (unitLIE lit_inst, instToId lit_inst)
+instance Ord Inst where
+  compare = cmpInst
+
+instance Eq Inst where
+  (==) i1 i2 = case i1 `cmpInst` i2 of
+                EQ    -> True
+                other -> False
+
+cmpInst  (Dict _ clas1 tys1 _ _) (Dict _ clas2 tys2 _ _)
+  = (clas1 `compare` clas2) `thenCmp` (tys1 `compare` tys2)
+cmpInst (Dict _ _ _ _ _) other
+  = LT
+
+
+cmpInst (Method _ _ _ _ _ _ _) (Dict _ _ _ _ _)
+  = GT
+cmpInst (Method _ id1 tys1 _ _ _ _) (Method _ id2 tys2 _ _ _ _)
+  = (id1 `compare` id2) `thenCmp` (tys1 `compare` tys2)
+cmpInst (Method _ _ _ _ _ _ _) other
+  = LT
+
+cmpInst (LitInst _ lit1 ty1 _ _) (LitInst _ lit2 ty2 _ _)
+  = (lit1 `cmpOverLit` lit2) `thenCmp` (ty1 `compare` ty2)
+cmpInst (LitInst _ _ _ _ _) other
+  = GT
+
+cmpOverLit (OverloadedIntegral   i1) (OverloadedIntegral   i2) = i1 `compare` i2
+cmpOverLit (OverloadedFractional f1) (OverloadedFractional f2) = f1 `compare` f2
+cmpOverLit (OverloadedIntegral _)    (OverloadedFractional _)  = LT
+cmpOverLit (OverloadedFractional _)  (OverloadedIntegral _)    = GT
 \end{code}
 
 
+Selection
+~~~~~~~~~
 \begin{code}
-instToId :: Inst s -> TcIdOcc s
-instToId (Dict u clas ty orig loc)
-  = TcId (mkInstId u (mkDictTy clas ty) (mkLocalName u SLIT("dict") loc))
-instToId (Method u id tys rho_ty orig loc)
-  = TcId (mkInstId u tau_ty (mkLocalName u (getLocalName id) loc))
-  where
-    (_, tau_ty) = splitRhoTy rho_ty    -- NB The method Id has just the tau type
-instToId (LitInst u list ty orig loc)
-  = TcId (mkInstId u ty (mkLocalName u SLIT("lit") loc))
-\end{code}
+instOrigin (Dict   u clas tys    origin loc) = origin
+instOrigin (Method u clas ty _ _ origin loc) = origin
+instOrigin (LitInst u lit ty     origin loc) = origin
 
-\begin{code}
-instType :: Inst s -> TcType s
-instType (Dict _ clas ty _ _)     = mkDictTy clas ty
-instType (LitInst _ _ ty _ _)     = ty
-instType (Method _ id tys ty _ _) = ty
-\end{code}
+instLoc (Dict   u clas tys    origin loc) = loc
+instLoc (Method u clas ty _ _ origin loc) = loc
+instLoc (LitInst u lit ty     origin loc) = loc
 
+getDictClassTys (Dict u clas tys _ _) = (clas, tys)
 
-Zonking
-~~~~~~~
-Zonking makes sure that the instance types are fully zonked,
-but doesn't do the same for the Id in a Method.  There's no
-need, and it's a lot of extra work.
+tyVarsOfInst :: Inst -> TcTyVarSet
+tyVarsOfInst (Dict _ _ tys _ _)        = tyVarsOfTypes  tys
+tyVarsOfInst (Method _ id tys _ _ _ _) = tyVarsOfTypes tys `unionVarSet` idFreeTyVars id
+                                        -- The id might have free type variables; in the case of
+                                        -- locally-overloaded class methods, for example
+tyVarsOfInst (LitInst _ _ ty _ _)     = tyVarsOfType  ty
+\end{code}
 
+Predicates
+~~~~~~~~~~
 \begin{code}
-zonkInst :: Inst s -> NF_TcM s (Inst s)
-zonkInst (Dict u clas ty orig loc)
-  = zonkTcType ty                      `thenNF_Tc` \ new_ty ->
-    returnNF_Tc (Dict u clas new_ty orig loc)
+isDict :: Inst -> Bool
+isDict (Dict _ _ _ _ _) = True
+isDict other           = False
 
-zonkInst (Method u id tys rho orig loc)                -- Doesn't zonk the id!
-  = mapNF_Tc zonkTcType tys            `thenNF_Tc` \ new_tys ->
-    zonkTcType rho                     `thenNF_Tc` \ new_rho ->
-    returnNF_Tc (Method u id new_tys new_rho orig loc)
+isMethodFor :: TcIdSet -> Inst -> Bool
+isMethodFor ids (Method uniq id tys _ _ orig loc) 
+  = id `elemVarSet` ids
+isMethodFor ids inst 
+  = False
 
-zonkInst (LitInst u lit ty orig loc)
-  = zonkTcType ty                      `thenNF_Tc` \ new_ty ->
-    returnNF_Tc (LitInst u lit new_ty orig loc)
+isTyVarDict :: Inst -> Bool
+isTyVarDict (Dict _ _ tys _ _) = all isTyVarTy tys
+isTyVarDict other             = False
+
+isStdClassTyVarDict (Dict _ clas [ty] _ _) = isStandardClass clas && isTyVarTy ty
+isStdClassTyVarDict other                 = False
 \end{code}
 
+Two predicates which deal with the case where class constraints don't
+necessarily result in bindings.  The first tells whether an @Inst@
+must be witnessed by an actual binding; the second tells whether an
+@Inst@ can be generalised over.
 
 \begin{code}
-tyVarsOfInst :: Inst s -> TcTyVarSet s
-tyVarsOfInst (Dict _ _ ty _ _)        = tyVarsOfType  ty
-tyVarsOfInst (Method _ _ tys rho _ _) = tyVarsOfTypes tys
-tyVarsOfInst (LitInst _ _ ty _ _)     = tyVarsOfType  ty
+instBindingRequired :: Inst -> Bool
+instBindingRequired (Dict _ clas _ _ _) = not (isNoDictClass clas)
+instBindingRequired other              = True
+
+instCanBeGeneralised :: Inst -> Bool
+instCanBeGeneralised (Dict _ clas _ _ _) = not (isCcallishClass clas)
+instCanBeGeneralised other              = True
 \end{code}
 
-@matchesInst@ checks when two @Inst@s are instances of the same
-thing at the same type, even if their uniques differ.
+
+Construction
+~~~~~~~~~~~~
 
 \begin{code}
-matchesInst :: Inst s -> Inst s -> Bool
+newDicts :: InstOrigin
+        -> TcThetaType
+        -> NF_TcM s (LIE, [TcId])
+newDicts orig theta
+  = tcGetSrcLoc                                `thenNF_Tc` \ loc ->
+    newDictsAtLoc orig loc theta        `thenNF_Tc` \ (dicts, ids) ->
+    returnNF_Tc (listToBag dicts, ids)
+
+-- Local function, similar to newDicts, 
+-- but with slightly different interface
+newDictsAtLoc :: InstOrigin
+              -> SrcLoc
+             -> TcThetaType
+             -> NF_TcM s ([Inst], [TcId])
+newDictsAtLoc orig loc theta =
+ tcGetUniques (length theta)           `thenNF_Tc` \ new_uniqs ->
+ let
+  mk_dict u (clas, tys) = Dict u clas tys orig loc
+  dicts = zipWithEqual "newDictsAtLoc" mk_dict new_uniqs theta
+ in
+ returnNF_Tc (dicts, map instToId dicts)
+
+newDictFromOld :: Inst -> Class -> [TcType] -> NF_TcM s Inst
+newDictFromOld (Dict _ _ _ orig loc) clas tys
+  = tcGetUnique              `thenNF_Tc` \ uniq ->
+    returnNF_Tc (Dict uniq clas tys orig loc)
+
+
+newMethod :: InstOrigin
+         -> TcId
+         -> [TcType]
+         -> NF_TcM s (LIE, TcId)
+newMethod orig id tys
+  =    -- Get the Id type and instantiate it at the specified types
+    let
+       (tyvars, rho) = splitForAllTys (idType id)
+       rho_ty        = substTy (mkTyVarSubst tyvars tys) rho
+       (theta, tau)  = splitRhoTy rho_ty
+    in
+    newMethodWithGivenTy orig id tys theta tau `thenNF_Tc` \ meth_inst ->
+    returnNF_Tc (unitLIE meth_inst, instToId meth_inst)
+
+instOverloadedFun orig (HsVar v) arg_tys theta tau
+  = newMethodWithGivenTy orig v arg_tys theta tau      `thenNF_Tc` \ inst ->
+    returnNF_Tc (HsVar (instToId inst), unitLIE inst)
+
+newMethodWithGivenTy orig id tys theta tau
+  = tcGetSrcLoc                `thenNF_Tc` \ loc ->
+    tcGetUnique                `thenNF_Tc` \ new_uniq ->
+    let
+       meth_inst = Method new_uniq id tys theta tau orig loc
+    in
+    returnNF_Tc meth_inst
+
+newMethodAtLoc :: InstOrigin -> SrcLoc
+              -> Id -> [TcType]
+              -> NF_TcM s (Inst, TcId)
+newMethodAtLoc orig loc real_id tys    -- Local function, similar to newMethod but with 
+                                       -- slightly different interface
+  =    -- Get the Id type and instantiate it at the specified types
+    tcGetUnique                                        `thenNF_Tc` \ new_uniq ->
+    let
+       (tyvars,rho) = splitForAllTys (idType real_id)
+       rho_ty        = ASSERT( length tyvars == length tys )
+                       substTy (mkTopTyVarSubst tyvars tys) rho
+       (theta, tau)  = splitRhoTy rho_ty
+       meth_inst     = Method new_uniq real_id tys theta tau orig loc
+    in
+    returnNF_Tc (meth_inst, instToId meth_inst)
+\end{code}
+
+In newOverloadedLit we convert directly to an Int or Integer if we
+know that's what we want.  This may save some time, by not
+temporarily generating overloaded literals, but it won't catch all
+cases (the rest are caught in lookupInst).
 
-matchesInst (Dict _ clas1 ty1 _ _) (Dict _ clas2 ty2 _ _)
-  = clas1 == clas2 && ty1 `eqSimpleTy` ty2
+\begin{code}
+newOverloadedLit :: InstOrigin
+                -> OverloadedLit
+                -> TcType
+                -> NF_TcM s (TcExpr, LIE)
+newOverloadedLit orig (OverloadedIntegral i) ty
+  | isIntTy ty && inIntRange i         -- Short cut for Int
+  = returnNF_Tc (int_lit, emptyLIE)
 
-matchesInst (Method _ id1 tys1 _ _ _) (Method _ id2 tys2 _ _ _)
-  =  id1 == id2
-  && and (zipWith eqSimpleTy tys1 tys2)
-  && length tys1 == length tys2
+  | isIntegerTy ty                     -- Short cut for Integer
+  = returnNF_Tc (integer_lit, emptyLIE)
 
-matchesInst (LitInst _ lit1 ty1 _ _) (LitInst _ lit2 ty2 _ _)
-  = lit1 `eq` lit2 && ty1 `eqSimpleTy` ty2
   where
-    (OverloadedIntegral   i1) `eq` (OverloadedIntegral   i2) = i1 == i2
-    (OverloadedFractional f1) `eq` (OverloadedFractional f2) = f1 == f2
-    _                        `eq` _                         = False
+    intprim_lit    = HsLitOut (HsIntPrim i) intPrimTy
+    integer_lit    = HsLitOut (HsInt i) integerTy
+    int_lit        = HsCon intDataCon [] [intprim_lit]
 
-matchesInst other1 other2 = False
+newOverloadedLit orig lit ty           -- The general case
+  = tcGetSrcLoc                        `thenNF_Tc` \ loc ->
+    tcGetUnique                        `thenNF_Tc` \ new_uniq ->
+    let
+       lit_inst = LitInst new_uniq lit ty orig loc
+    in
+    returnNF_Tc (HsVar (instToId lit_inst), unitLIE lit_inst)
 \end{code}
 
 
-Predicates
-~~~~~~~~~~
 \begin{code}
-isDict :: Inst s -> Bool
-isDict (Dict _ _ _ _ _) = True
-isDict other           = False
-
-isTyVarDict :: Inst s -> Bool
-isTyVarDict (Dict _ _ ty _ _) = isTyVarTy ty
-isTyVarDict other            = False
+instToId :: Inst -> TcId
+instToId inst = instToIdBndr inst
+
+instToIdBndr :: Inst -> TcId
+instToIdBndr (Dict u clas ty orig loc)
+  = mkUserLocal (mkDictOcc (getOccName clas)) u (mkDictTy clas ty) loc
+
+instToIdBndr (Method u id tys theta tau orig loc)
+  = mkUserLocal (mkMethodOcc (getOccName id)) u tau loc
+    
+instToIdBndr (LitInst u list ty orig loc)
+  = mkSysLocal SLIT("lit") u ty
 \end{code}
 
-Two predicates which deal with the case where class constraints don't
-necessarily result in bindings.  The first tells whether an @Inst@
-must be witnessed by an actual binding; the second tells whether an
-@Inst@ can be generalised over.
+
+Zonking
+~~~~~~~
+Zonking makes sure that the instance types are fully zonked,
+but doesn't do the same for the Id in a Method.  There's no
+need, and it's a lot of extra work.
 
 \begin{code}
-instBindingRequired :: Inst s -> Bool
-instBindingRequired inst
-  = case getInstOrigin inst of
-       CCallOrigin _ _   -> False      -- No binding required
-       LitLitOrigin  _   -> False
-       OccurrenceOfCon _ -> False
-       other             -> True
-
-instCanBeGeneralised :: Inst s -> Bool
-instCanBeGeneralised inst
-  = case getInstOrigin inst of
-       CCallOrigin _ _ -> False        -- Can't be generalised
-       LitLitOrigin  _ -> False        -- Can't be generalised
-       other           -> True
+zonkInst :: Inst -> NF_TcM s Inst
+zonkInst (Dict u clas tys orig loc)
+  = zonkTcTypes        tys                     `thenNF_Tc` \ new_tys ->
+    returnNF_Tc (Dict u clas new_tys orig loc)
+
+zonkInst (Method u id tys theta tau orig loc) 
+  = zonkId id                  `thenNF_Tc` \ new_id ->
+       -- Essential to zonk the id in case it's a local variable
+       -- Can't use zonkIdOcc because the id might itself be
+       -- an InstId, in which case it won't be in scope
+
+    zonkTcTypes tys            `thenNF_Tc` \ new_tys ->
+    zonkTcThetaType theta      `thenNF_Tc` \ new_theta ->
+    zonkTcType tau             `thenNF_Tc` \ new_tau ->
+    returnNF_Tc (Method u new_id new_tys new_theta new_tau orig loc)
+
+zonkInst (LitInst u lit ty orig loc)
+  = zonkTcType ty                      `thenNF_Tc` \ new_ty ->
+    returnNF_Tc (LitInst u lit new_ty orig loc)
 \end{code}
 
 
@@ -340,45 +426,47 @@ ToDo: improve these pretty-printing things.  The ``origin'' is really only
 relevant in error messages.
 
 \begin{code}
-instance Outputable (Inst s) where
-    ppr sty (LitInst uniq lit ty orig loc)
-      = ppHang (ppSep [case lit of
-                         OverloadedIntegral   i -> ppInteger i
-                         OverloadedFractional f -> ppRational f,
-                      ppStr "at",
-                      ppr sty ty,
-                      show_uniq sty uniq
-               ])
-         4 (show_origin sty orig)
-
-    ppr sty (Dict uniq clas ty orig loc)
-      = ppHang (ppSep [ppr sty clas, 
-                      ppStr "at",
-                      ppr sty ty,
-                      show_uniq sty uniq
-               ])
-         4 (show_origin sty orig)
-
-    ppr sty (Method uniq id tys rho orig loc)
-      = ppHang (ppSep [ppr sty id, 
-                      ppStr "at",
-                      ppr sty tys,
-                      show_uniq sty uniq
-               ])
-         4 (show_origin sty orig)
-
-show_uniq PprDebug uniq = ppr PprDebug uniq
-show_uniq sty     uniq = ppNil
-
-show_origin sty orig    = ppBesides [ppLparen, pprOrigin sty orig, ppRparen]
-\end{code}
+instance Outputable Inst where
+    ppr inst = pprInst inst
+
+pprInst (LitInst u lit ty orig loc)
+  = hsep [case lit of
+             OverloadedIntegral   i -> integer i
+             OverloadedFractional f -> rational f,
+          ptext SLIT("at"),
+          ppr ty,
+          show_uniq u]
+
+pprInst (Dict u clas tys orig loc) = pprConstraint clas tys <+> show_uniq u
+
+pprInst (Method u id tys _ _ orig loc)
+  = hsep [ppr id, ptext SLIT("at"), 
+         brackets (interppSP tys),
+         show_uniq u]
+
+tidyInst :: TidyEnv -> Inst -> (TidyEnv, Inst)
+tidyInst env (LitInst u lit ty orig loc)
+  = (env', LitInst u lit ty' orig loc)
+  where
+    (env', ty') = tidyOpenType env ty
 
-Printing in error messages
+tidyInst env (Dict u clas tys orig loc)
+  = (env', Dict u clas tys' orig loc)
+  where
+    (env', tys') = tidyOpenTypes env tys
 
-\begin{code}
-noInstanceErr inst sty = ppHang (ppPStr SLIT("No instance for:")) 4 (ppr sty inst)
+tidyInst env (Method u id tys theta tau orig loc)
+  = (env', Method u id tys' theta tau orig loc)
+               -- Leave theta, tau alone cos we don't print them
+  where
+    (env', tys') = tidyOpenTypes env tys
+    
+tidyInsts env insts = mapAccumL tidyInst env insts
+
+show_uniq u = ifPprDebug (text "{-" <> ppr u <> text "-}")
 \end{code}
 
+
 %************************************************************************
 %*                                                                     *
 \subsection[InstEnv-types]{Type declarations}
@@ -386,7 +474,7 @@ noInstanceErr inst sty = ppHang (ppPStr SLIT("No instance for:")) 4 (ppr sty ins
 %************************************************************************
 
 \begin{code}
-type InstanceMapper = Class -> (ClassInstEnv, ClassOp -> SpecEnv)
+type InstanceMapper = Class -> InstEnv
 \end{code}
 
 A @ClassInstEnv@ lives inside a class, and identifies all the instances
@@ -405,63 +493,99 @@ The "a" in the pattern must be one of the forall'd variables in
 the dfun type.
 
 \begin{code}
-lookupInst :: Inst s 
-          -> TcM s ([Inst s], 
-                    (TcIdOcc s, TcExpr s))     -- The new binding
+data LookupInstResult s
+  = NoInstance
+  | SimpleInst TcExpr          -- Just a variable, type application, or literal
+  | GenInst    [Inst] TcExpr   -- The expression and its needed insts
+
+lookupInst :: Inst 
+          -> NF_TcM s (LookupInstResult s)
 
 -- Dictionaries
 
-lookupInst dict@(Dict _ clas ty orig loc)
-  = case lookupMEnv matchTy (get_inst_env clas orig) ty of
-      Nothing  -> failTc (noInstanceErr dict)
+lookupInst dict@(Dict _ clas tys orig loc)
+  = case lookupInstEnv (ppr clas) (classInstEnv clas) tys of
 
-      Just (dfun_id, tenv) 
+      Just (tenv, dfun_id)
        -> let
-               (tyvars, rho) = splitForAllTy (idType dfun_id)
-               ty_args       = map (assoc "lookupInst" tenv) tyvars
-               -- tenv should bind all the tyvars
-          in
-          tcInstType tenv rho          `thenNF_Tc` \ dfun_rho ->
-          let
-               (theta, tau) = splitRhoTy dfun_rho
+               subst         = mkSubst (tyVarsOfTypes tys) tenv
+               (tyvars, rho) = splitForAllTys (idType dfun_id)
+               ty_args       = map subst_tv tyvars
+               dfun_rho      = substTy subst rho
+               (theta, tau)  = splitRhoTy dfun_rho
+               ty_app        = mkHsTyApp (HsVar dfun_id) ty_args
+               subst_tv tv   = case lookupSubstEnv tenv tv of
+                                  Just (DoneTy ty)  -> ty
+                                       -- tenv should bind all the tyvars
           in
+          if null theta then
+               returnNF_Tc (SimpleInst ty_app)
+          else
           newDictsAtLoc orig loc theta `thenNF_Tc` \ (dicts, dict_ids) ->
           let 
-               rhs = mkHsDictApp (mkHsTyApp (HsVar (RealId dfun_id)) ty_args) dict_ids
+               rhs = mkHsDictApp ty_app dict_ids
           in
-          returnTc (dicts, (instToId dict, rhs))
+          returnNF_Tc (GenInst dicts rhs)
                             
+      Nothing  -> returnNF_Tc NoInstance
 
 -- Methods
 
-lookupInst inst@(Method _ id tys rho orig loc)
+lookupInst inst@(Method _ id tys theta _ orig loc)
   = newDictsAtLoc orig loc theta       `thenNF_Tc` \ (dicts, dict_ids) ->
-    returnTc (dicts, (instToId inst, mkHsDictApp (mkHsTyApp (HsVar id) tys) dict_ids))
-  where
-    (theta,_) = splitRhoTy rho
+    returnNF_Tc (GenInst dicts (mkHsDictApp (mkHsTyApp (HsVar id) tys) dict_ids))
 
 -- Literals
 
 lookupInst inst@(LitInst u (OverloadedIntegral i) ty orig loc)
-  | i >= toInteger minInt && i <= toInteger maxInt
-  =    -- It's overloaded but small enough to fit into an Int
-    tcLookupGlobalValueByKey fromIntClassOpKey `thenNF_Tc` \ from_int ->
-    newMethodAtLoc orig loc from_int [ty]              `thenNF_Tc` \ (method_inst, method_id) ->
-    returnTc ([method_inst], (instToId inst, HsApp (HsVar method_id) int_lit))
+  | isIntTy ty && in_int_range                 -- Short cut for Int
+  = returnNF_Tc (GenInst [] int_lit)
+       -- GenInst, not SimpleInst, because int_lit is actually a constructor application
 
-  | otherwise 
-  =     -- Alas, it is overloaded and a big literal!
-    tcLookupGlobalValueByKey fromIntegerClassOpKey     `thenNF_Tc` \ from_integer ->
+  | isIntegerTy ty                             -- Short cut for Integer
+  = returnNF_Tc (GenInst [] integer_lit)
+
+  | in_int_range                               -- It's overloaded but small enough to fit into an Int
+  = tcLookupValueByKey fromIntClassOpKey       `thenNF_Tc` \ from_int ->
+    newMethodAtLoc orig loc from_int [ty]      `thenNF_Tc` \ (method_inst, method_id) ->
+    returnNF_Tc (GenInst [method_inst] (HsApp (HsVar method_id) int_lit))
+
+  | otherwise                                  -- Alas, it is overloaded and a big literal!
+  = tcLookupValueByKey fromIntegerClassOpKey   `thenNF_Tc` \ from_integer ->
     newMethodAtLoc orig loc from_integer [ty]          `thenNF_Tc` \ (method_inst, method_id) ->
-    returnTc ([method_inst], (instToId inst, HsApp (HsVar method_id) (HsLitOut (HsInt i) ty)))
+    returnNF_Tc (GenInst [method_inst] (HsApp (HsVar method_id) integer_lit))
   where
+    in_int_range   = inIntRange i
     intprim_lit    = HsLitOut (HsIntPrim i) intPrimTy
-    int_lit        = HsApp (HsVar (RealId intDataCon)) intprim_lit
+    integer_lit    = HsLitOut (HsInt i) integerTy
+    int_lit        = HsCon intDataCon [] [intprim_lit]
+
+-- similar idea for overloaded floating point literals: if the literal is
+-- *definitely* a float or a double, generate the real thing here.
+-- This is essential  (see nofib/spectral/nucleic).
 
 lookupInst inst@(LitInst u (OverloadedFractional f) ty orig loc)
-  = tcLookupGlobalValueByKey fromRationalClassOpKey    `thenNF_Tc` \ from_rational ->
+  | isFloatTy ty    = returnNF_Tc (GenInst [] float_lit)
+  | isDoubleTy ty   = returnNF_Tc (GenInst [] double_lit)
+
+  | otherwise 
+         = tcLookupValueByKey fromRationalClassOpKey   `thenNF_Tc` \ from_rational ->
+
+       -- The type Rational isn't wired in so we have to conjure it up
+    tcLookupTyConByKey rationalTyConKey        `thenNF_Tc` \ rational_tycon ->
+    let
+       rational_ty  = mkSynTy rational_tycon []
+       rational_lit = HsLitOut (HsFrac f) rational_ty
+    in
     newMethodAtLoc orig loc from_rational [ty]         `thenNF_Tc` \ (method_inst, method_id) ->
-    returnTc ([method_inst], (instToId inst, HsApp (HsVar method_id) (HsLitOut (HsFrac f) ty)))
+    returnNF_Tc (GenInst [method_inst] (HsApp (HsVar method_id) rational_lit))
+
+  where
+    floatprim_lit  = HsLitOut (HsFloatPrim f) floatPrimTy
+    float_lit      = HsCon floatDataCon [] [floatprim_lit]
+    doubleprim_lit = HsLitOut (HsDoublePrim f) doublePrimTy
+    double_lit     = HsCon doubleDataCon [] [doubleprim_lit]
+
 \end{code}
 
 There is a second, simpler interface, when you want an instance of a
@@ -470,55 +594,19 @@ appropriate dictionary if it exists.  It is used only when resolving
 ambiguous dictionaries.
 
 \begin{code}
-lookupClassInstAtSimpleType :: Class -> Type -> Maybe Id
-
-lookupClassInstAtSimpleType clas ty
-  = case (lookupMEnv matchTy (getClassInstEnv clas) ty) of
-      Nothing      -> Nothing
-      Just (dfun,_) -> ASSERT( null tyvars && null theta )
-                      Just dfun
-                   where
-                      (tyvars, theta, _) = splitSigmaTy (idType dfun)
-\end{code}
-
-
-@mkInstSpecEnv@ is used to construct the @SpecEnv@ for a dfun.
-It does it by filtering the class's @InstEnv@.  All pretty shady stuff.
-
-\begin{code}
-mkInstSpecEnv clas inst_ty inst_tvs inst_theta = panic "mkInstSpecEnv"
-\end{code}
-
-\begin{pseudocode}
-mkInstSpecEnv :: Class                 -- class
-             -> Type                   -- instance type
-             -> [TyVarTemplate]        -- instance tyvars
-             -> ThetaType              -- superclasses dicts
-             -> SpecEnv                -- specenv for dfun of instance
-
-mkInstSpecEnv clas inst_ty inst_tvs inst_theta
-  = mkSpecEnv (catMaybes (map maybe_spec_info matches))
-  where
-    matches = matchMEnv matchTy (getClassInstEnv clas) inst_ty
-
-    maybe_spec_info (_, match_info, MkInstTemplate dfun _ [])
-      = Just (SpecInfo (map (assocMaybe match_info) inst_tvs) (length inst_theta) dfun)
-    maybe_spec_info (_, match_info, _)
-      = Nothing
-\end{pseudocode}
-
-
-\begin{code}
-addClassInst
-    :: ClassInstEnv            -- Incoming envt
-    -> Type                    -- The instance type: inst_ty
-    -> Id                      -- Dict fun id to apply. Free tyvars of inst_ty must
-                               -- be the same as the forall'd tyvars of the dfun id.
-    -> MaybeErr
-         ClassInstEnv          -- Success
-         (Type, Id)            -- Offending overlap
-
-addClassInst inst_env inst_ty dfun_id = insertMEnv matchTy inst_env inst_ty dfun_id
+lookupSimpleInst :: InstEnv
+                -> Class
+                -> [Type]                      -- Look up (c,t)
+                -> NF_TcM s (Maybe ThetaType)          -- Here are the needed (c,t)s
+
+lookupSimpleInst class_inst_env clas tys
+  = case lookupInstEnv (ppr clas) class_inst_env tys of
+      Nothing   -> returnNF_Tc Nothing
+
+      Just (tenv, dfun)
+       -> returnNF_Tc (Just (substTheta (mkSubst emptyInScopeSet tenv) theta))
+        where
+          (_, theta, _) = splitSigmaTy (idType dfun)
 \end{code}
 
 
@@ -534,8 +622,8 @@ This is important for decent error message reporting because dictionaries
 don't appear in the original source code.  Doubtless this type will evolve...
 
 \begin{code}
-data InstOrigin s
-  = OccurrenceOf (TcIdOcc s)   -- Occurrence of an overloaded identifier
+data InstOrigin
+  = OccurrenceOf TcId  -- Occurrence of an overloaded identifier
   | OccurrenceOfCon Id         -- Occurrence of a data constructor
 
   | RecordUpdOrigin
@@ -546,25 +634,19 @@ data InstOrigin s
 
   | LiteralOrigin      HsLit   -- Occurrence of a literal
 
+  | PatOrigin RenamedPat
+
   | ArithSeqOrigin     RenamedArithSeqInfo -- [x..], [x..y] etc
 
   | SignatureOrigin            -- A dict created from a type signature
+  | Rank2Origin                        -- A dict created when typechecking the argument
+                               -- of a rank-2 typed function
 
   | DoOrigin                   -- The monad for a do expression
 
   | ClassDeclOrigin            -- Manufactured during a class decl
 
-  | DerivingOrigin     InstanceMapper
-                       Class
-                       TyCon
-
-       -- During "deriving" operations we have an ever changing
-       -- mapping of classes to instances, so we record it inside the
-       -- origin information.  This is a bit of a hack, but it works
-       -- fine.  (Simon is to blame [WDP].)
-
-  | InstanceSpecOrigin InstanceMapper
-                       Class   -- in a SPECIALIZE instance pragma
+  | InstanceSpecOrigin Class   -- in a SPECIALIZE instance pragma
                        Type
 
        -- When specialising instances the instance info attached to
@@ -572,8 +654,6 @@ data InstOrigin s
        -- origin information.  This is a bit of a hack, but it works
        -- fine.  (Patrick is to blame [WDP].)
 
-  | DefaultDeclOrigin          -- Related to a `default' declaration
-
   | ValSpecOrigin      Name    -- in a SPECIALIZE pragma for a value
 
        -- Argument or result of a ccall
@@ -591,64 +671,47 @@ data InstOrigin s
 \end{code}
 
 \begin{code}
--- During deriving and instance specialisation operations
--- we can't get the instances of the class from inside the
--- class, because the latter ain't ready yet.  Instead we
--- find a mapping from classes to envts inside the dict origin.
-
-get_inst_env :: Class -> InstOrigin s -> ClassInstEnv
-get_inst_env clas (DerivingOrigin inst_mapper _ _)
-  = fst (inst_mapper clas)
-get_inst_env clas (InstanceSpecOrigin inst_mapper _ _)
-  = fst (inst_mapper clas)
-get_inst_env clas other_orig = getClassInstEnv clas
-
-
-pprOrigin :: PprStyle -> InstOrigin s -> Pretty
-
-pprOrigin sty (OccurrenceOf id)
-      = ppBesides [ppPStr SLIT("at a use of an overloaded identifier: `"),
-                  ppr sty id, ppChar '\'']
-pprOrigin sty (OccurrenceOfCon id)
-      = ppBesides [ppPStr SLIT("at a use of an overloaded constructor: `"),
-                  ppr sty id, ppChar '\'']
-pprOrigin sty (InstanceDeclOrigin)
-      = ppStr "in an instance declaration"
-pprOrigin sty (LiteralOrigin lit)
-      = ppCat [ppStr "at an overloaded literal:", ppr sty lit]
-pprOrigin sty (ArithSeqOrigin seq)
-      = ppCat [ppStr "at an arithmetic sequence:", ppr sty seq]
-pprOrigin sty (SignatureOrigin)
-      = ppStr "in a type signature"
-pprOrigin sty (DoOrigin)
-      = ppStr "in a do statement"
-pprOrigin sty (ClassDeclOrigin)
-      = ppStr "in a class declaration"
-pprOrigin sty (DerivingOrigin _ clas tycon)
-      = ppBesides [ppStr "in a `deriving' clause; class `",
-                         ppr sty clas,
-                         ppStr "'; offending type `",
-                         ppr sty tycon,
-                         ppStr "'"]
-pprOrigin sty (InstanceSpecOrigin _ clas ty)
-      = ppBesides [ppStr "in a SPECIALIZE instance pragma; class \"",
-                  ppr sty clas, ppStr "\" type: ", ppr sty ty]
-pprOrigin sty (DefaultDeclOrigin)
-      = ppStr "in a `default' declaration"
-pprOrigin sty (ValSpecOrigin name)
-      = ppBesides [ppStr "in a SPECIALIZE user-pragma for `",
-                  ppr sty name, ppStr "'"]
-pprOrigin sty (CCallOrigin clabel Nothing{-ccall result-})
-      = ppBesides [ppStr "in the result of the _ccall_ to `",
-                  ppStr clabel, ppStr "'"]
-pprOrigin sty (CCallOrigin clabel (Just arg_expr))
-      = ppBesides [ppStr "in an argument in the _ccall_ to `",
-                 ppStr clabel, ppStr "', namely: ", ppr sty arg_expr]
-pprOrigin sty (LitLitOrigin s)
-      = ppBesides [ppStr "in this ``literal-literal'': ", ppStr s]
-pprOrigin sty UnknownOrigin
-      = ppStr "in... oops -- I don't know where the overloading came from!"
+pprOrigin :: Inst -> SDoc
+pprOrigin inst
+  = hsep [text "arising from", pp_orig orig, text "at", ppr locn]
+  where
+    (orig, locn) = case inst of
+                       Dict _ _ _       orig loc -> (orig,loc)
+                       Method _ _ _ _ _ orig loc -> (orig,loc)
+                       LitInst _ _ _    orig loc -> (orig,loc)
+                       
+    pp_orig (OccurrenceOf id)
+       = hsep [ptext SLIT("use of"), quotes (ppr id)]
+    pp_orig (OccurrenceOfCon id)
+       = hsep [ptext SLIT("use of"), quotes (ppr id)]
+    pp_orig (LiteralOrigin lit)
+       = hsep [ptext SLIT("the literal"), quotes (ppr lit)]
+    pp_orig (PatOrigin pat)
+       = hsep [ptext SLIT("the pattern"), quotes (ppr pat)]
+    pp_orig (InstanceDeclOrigin)
+       =  ptext SLIT("an instance declaration")
+    pp_orig (ArithSeqOrigin seq)
+       = hsep [ptext SLIT("the arithmetic sequence"), quotes (ppr seq)]
+    pp_orig (SignatureOrigin)
+       =  ptext SLIT("a type signature")
+    pp_orig (Rank2Origin)
+       =  ptext SLIT("a function with an overloaded argument type")
+    pp_orig (DoOrigin)
+       =  ptext SLIT("a do statement")
+    pp_orig (ClassDeclOrigin)
+       =  ptext SLIT("a class declaration")
+    pp_orig (InstanceSpecOrigin clas ty)
+       = hsep [text "a SPECIALIZE instance pragma; class",
+               quotes (ppr clas), text "type:", ppr ty]
+    pp_orig (ValSpecOrigin name)
+       = hsep [ptext SLIT("a SPECIALIZE user-pragma for"), quotes (ppr name)]
+    pp_orig (CCallOrigin clabel Nothing{-ccall result-})
+       = hsep [ptext SLIT("the result of the _ccall_ to"), quotes (text clabel)]
+    pp_orig (CCallOrigin clabel (Just arg_expr))
+       = hsep [ptext SLIT("an argument in the _ccall_ to"), quotes (text clabel) <> comma, 
+               text "namely", quotes (ppr arg_expr)]
+    pp_orig (LitLitOrigin s)
+       = hsep [ptext SLIT("the ``literal-literal''"), quotes (text s)]
+    pp_orig (UnknownOrigin)
+       = ptext SLIT("...oops -- I don't know where the overloading came from!")
 \end{code}
-
-
-