Refactor the invariants for ClsInsts
authorSimon Peyton Jones <simonpj@microsoft.com>
Tue, 1 Jan 2013 23:09:32 +0000 (23:09 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Tue, 1 Jan 2013 23:09:32 +0000 (23:09 +0000)
We now have the invariant for a ClsInst that the is_tvs field
is always completely fresh type variables. See
Note [Template tyvars are fresh] in InstEnv.

(Previously we frehened them when extending the instance environment,
but that seems messier because it was an invariant only when the
ClsInst was in an InstEnv.  Moreover, there was an invariant that
thet tyvars of the DFunid in the ClsInst had to match, and I have
removed that invariant altogether; there is no need for it.)

Other changes I made at the same time:

 * Make is_tvs into a *list*, in the right order for the dfun type
   arguments.  This removes the wierd need for the dfun to have the
   same tyvars as the ClsInst template, an invariant I have always
   hated. The cost is that we need to make it a VarSet when matching.
   We could cache an is_tv_set instead.

 * Add a cached is_cls field to the ClsInst, to save fishing
   the Class out of the DFun.  (Renamed is_cls to is_cls_nm.)

 * Make tcSplitDFunTy return the dfun args, not just the *number*
   of dfun args

 * Make InstEnv.instanceHead return just the *head* of the
   instance declaration.  Add instanceSig to return the whole
   thing.

13 files changed:
compiler/coreSyn/CoreSubst.lhs
compiler/coreSyn/CoreUnfold.lhs
compiler/iface/MkIface.lhs
compiler/main/TidyPgm.lhs
compiler/typecheck/Inst.lhs
compiler/typecheck/TcDeriv.lhs
compiler/typecheck/TcEnv.lhs
compiler/typecheck/TcGenGenerics.lhs
compiler/typecheck/TcInstDcls.lhs
compiler/typecheck/TcSplice.lhs
compiler/typecheck/TcType.lhs
compiler/types/FunDeps.lhs
compiler/types/InstEnv.lhs

index 89d1c6f..02aa562 100644 (file)
@@ -1192,7 +1192,7 @@ exprIsConApp_maybe id_unf expr
         -- Look through dictionary functions; see Note [Unfolding DFuns]
         | DFunUnfolding dfun_nargs con ops <- unfolding
         , length args == dfun_nargs    -- See Note [DFun arity check]
-        , let (dfun_tvs, _n_theta, _cls, dfun_res_tys) = tcSplitDFunTy (idType fun)
+        , let (dfun_tvs, _theta, _cls, dfun_res_tys) = tcSplitDFunTy (idType fun)
               subst    = zipOpenTvSubst dfun_tvs (stripTypeArgs (takeList dfun_tvs args))
               mk_arg (DFunPolyArg e) = mkApps e args
               mk_arg (DFunLamArg i)  = args !! i
index 70ddc9a..65235a6 100644 (file)
@@ -101,8 +101,8 @@ mkDFunUnfolding :: Type -> [DFunArg CoreExpr] -> Unfolding
 mkDFunUnfolding dfun_ty ops 
   = DFunUnfolding dfun_nargs data_con ops
   where
-    (tvs, n_theta, cls, _) = tcSplitDFunTy dfun_ty
-    dfun_nargs = length tvs + n_theta
+    (tvs, theta, cls, _) = tcSplitDFunTy dfun_ty
+    dfun_nargs = length tvs + length theta
     data_con   = classDataCon cls
 
 mkWwInlineRule :: Id -> CoreExpr -> Arity -> Unfolding
index 53e1a63..fed30f1 100644 (file)
@@ -1604,8 +1604,9 @@ getFS x = occNameFS (getOccName x)
 
 --------------------------
 instanceToIfaceInst :: ClsInst -> IfaceClsInst
-instanceToIfaceInst (ClsInst { is_dfun = dfun_id, is_flag = oflag,
-                                is_cls = cls_name, is_tcs = mb_tcs })
+instanceToIfaceInst (ClsInst { is_dfun = dfun_id, is_flag = oflag
+                             , is_cls_nm = cls_name, is_cls = cls
+                             , is_tys = tys, is_tcs = mb_tcs })
   = ASSERT( cls_name == className cls )
     IfaceClsInst { ifDFun    = dfun_name,
                 ifOFlag   = oflag,
@@ -1621,8 +1622,6 @@ instanceToIfaceInst (ClsInst { is_dfun = dfun_id, is_flag = oflag,
     is_local name = nameIsLocalOrFrom mod name
 
         -- Compute orphanhood.  See Note [Orphans] in IfaceSyn
-    (_, _, cls, tys) = tcSplitDFunTy (idType dfun_id)
-                -- Slightly awkward: we need the Class to get the fundeps
     (tvs, fds) = classTvsFds cls
     arg_names = [filterNameSet is_local (orphNamesOfType ty) | ty <- tys]
 
index 39ccd62..bc4c6b9 100644 (file)
@@ -136,7 +136,7 @@ mkBootModDetailsTc hsc_env
   = do  { let dflags = hsc_dflags hsc_env
         ; showPass dflags CoreTidy
 
-        ; let { insts'     = tidyInstances globaliseAndTidyId insts
+        ; let { insts'     = map (tidyClsInstDFun globaliseAndTidyId) insts
               ; dfun_ids   = map instanceDFunId insts'
               ; type_env1  = mkBootTypeEnv (availsToNameSet exports)
                                 (typeEnvIds type_env) tcs fam_insts
@@ -336,7 +336,7 @@ tidyProgram hsc_env  (ModGuts { mg_module    = mod
               ; tidy_type_env = tidyTypeEnv omit_prags
                                       (extendTypeEnvWithIds type_env final_ids)
 
-              ; tidy_insts    = tidyInstances (lookup_dfun tidy_type_env) insts
+              ; tidy_insts    = map (tidyClsInstDFun (lookup_dfun tidy_type_env)) insts
                 -- A DFunId will have a binding in tidy_binds, and so
                 -- will now be in final_env, replete with IdInfo
                 -- Its name will be unchanged since it was born, but
@@ -440,14 +440,6 @@ trimThing (AnId id)
 
 trimThing other_thing
   = other_thing
-
-
-tidyInstances :: (DFunId -> DFunId) -> [ClsInst] -> [ClsInst]
-tidyInstances tidy_dfun ispecs
-  = map tidy ispecs
-  where
-    tidy ispec = setInstanceDFunId ispec $
-                 tidy_dfun (instanceDFunId ispec)
 \end{code}
 
 \begin{code}
index 5b6364b..905a473 100644 (file)
@@ -414,64 +414,60 @@ addLocalInst :: InstEnv -> ClsInst -> TcM InstEnv
 -- Check that the proposed new instance is OK, 
 -- and then add it to the home inst env
 -- If overwrite_inst, then we can overwrite a direct match
-addLocalInst home_ie ispec = do
-    -- Instantiate the dfun type so that we extend the instance
-    -- envt with completely fresh template variables
-    -- This is important because the template variables must
-    -- not overlap with anything in the things being looked up
-    -- (since we do unification).  
-        --
-        -- We use tcInstSkolType because we don't want to allocate fresh
-        --  *meta* type variables.
-        --
-        -- We use UnkSkol --- and *not* InstSkol or PatSkol --- because
-        -- these variables must be bindable by tcUnifyTys.  See
-        -- the call to tcUnifyTys in InstEnv, and the special
-        -- treatment that instanceBindFun gives to isOverlappableTyVar
-        -- This is absurdly delicate.
-
-    let dfun = instanceDFunId ispec
-    (tvs', theta', tau') <- tcInstSkolType (idType dfun)
-    let (cls, tys') = tcSplitDFunHead tau'
-        dfun'      = setIdType dfun (mkSigmaTy tvs' theta' tau')           
-        ispec'      = setInstanceDFunId ispec dfun'
-
-        -- Load imported instances, so that we report
-        -- duplicates correctly
-    eps <- getEps
-    let inst_envs = (eps_inst_env eps, home_ie)
-
-        -- Check functional dependencies
-    case checkFunDeps inst_envs ispec' of
-        Just specs -> funDepErr ispec' specs
-        Nothing    -> return ()
-
-        -- Check for duplicate instance decls
-    let (matches, unifs, _) = lookupInstEnv inst_envs cls tys'
-        dup_ispecs = [ dup_ispec 
-                        | (dup_ispec, _) <- matches
-                        , let (_,_,_,dup_tys) = instanceHead dup_ispec
-                        , isJust (tcMatchTys (mkVarSet tvs') tys' dup_tys)]
-                        
-        -- Find memebers of the match list which ispec itself matches.
-        -- If the match is 2-way, it's a duplicate
-        -- If it's a duplicate, but we can overwrite home package dups, then overwrite
-    isGHCi <- getIsGHCi
-    overlapFlag <- getOverlapFlag
-    case isGHCi of
-        False -> case dup_ispecs of
-            dup : _ -> dupInstErr ispec' dup >> return (extendInstEnv home_ie ispec')
-            []      -> return (extendInstEnv home_ie ispec')
-        True  -> case (dup_ispecs, home_ie_matches, unifs, overlapFlag) of
-            (_, _:_, _, _)      -> return (overwriteInstEnv home_ie ispec')
-            (dup:_, [], _, _)   -> dupInstErr ispec' dup >> return (extendInstEnv home_ie ispec')
-            ([], _, u:_, NoOverlap _)    -> overlappingInstErr ispec' u >> return (extendInstEnv home_ie ispec')
-            _                   -> return (extendInstEnv home_ie ispec')
-          where (homematches, _) = lookupInstEnv' home_ie cls tys'
-                home_ie_matches = [ dup_ispec 
-                    | (dup_ispec, _) <- homematches
-                    , let (_,_,_,dup_tys) = instanceHead dup_ispec
-                    , isJust (tcMatchTys (mkVarSet tvs') tys' dup_tys)]
+addLocalInst home_ie ispec
+   = do {
+         -- Instantiate the dfun type so that we extend the instance
+         -- envt with completely fresh template variables
+         -- This is important because the template variables must
+         -- not overlap with anything in the things being looked up
+         -- (since we do unification).  
+             --
+             -- We use tcInstSkolType because we don't want to allocate fresh
+             --  *meta* type variables.
+             --
+             -- We use UnkSkol --- and *not* InstSkol or PatSkol --- because
+             -- these variables must be bindable by tcUnifyTys.  See
+             -- the call to tcUnifyTys in InstEnv, and the special
+             -- treatment that instanceBindFun gives to isOverlappableTyVar
+             -- This is absurdly delicate.
+
+             -- Load imported instances, so that we report
+             -- duplicates correctly
+           eps <- getEps
+         ; let inst_envs = (eps_inst_env eps, home_ie)
+               (tvs, cls, tys) = instanceHead ispec
+
+             -- Check functional dependencies
+         ; case checkFunDeps inst_envs ispec of
+             Just specs -> funDepErr ispec specs
+             Nothing    -> return ()
+
+             -- Check for duplicate instance decls
+         ; let (matches, unifs, _) = lookupInstEnv inst_envs cls tys
+               dup_ispecs = [ dup_ispec 
+                            | (dup_ispec, _) <- matches
+                            , let dup_tys = is_tys dup_ispec
+                            , isJust (tcMatchTys (mkVarSet tvs) tys dup_tys)]
+                             
+             -- Find memebers of the match list which ispec itself matches.
+             -- If the match is 2-way, it's a duplicate
+             -- If it's a duplicate, but we can overwrite home package dups, then overwrite
+         ; isGHCi <- getIsGHCi
+         ; overlapFlag <- getOverlapFlag
+         ; case isGHCi of
+             False -> case dup_ispecs of
+                 dup : _ -> dupInstErr ispec dup >> return (extendInstEnv home_ie ispec)
+                 []      -> return (extendInstEnv home_ie ispec)
+             True  -> case (dup_ispecs, home_ie_matches, unifs, overlapFlag) of
+                 (_, _:_, _, _)      -> return (overwriteInstEnv home_ie ispec)
+                 (dup:_, [], _, _)   -> dupInstErr ispec dup >> return (extendInstEnv home_ie ispec)
+                 ([], _, u:_, NoOverlap _)    -> overlappingInstErr ispec u >> return (extendInstEnv home_ie ispec)
+                 _                   -> return (extendInstEnv home_ie ispec)
+               where (homematches, _) = lookupInstEnv' home_ie cls tys
+                     home_ie_matches = [ dup_ispec 
+                         | (dup_ispec, _) <- homematches
+                         , let dup_tys = is_tys dup_ispec
+                         , isJust (tcMatchTys (mkVarSet tvs) tys dup_tys)] }
 
 traceDFuns :: [ClsInst] -> TcRn ()
 traceDFuns ispecs
index 68f327e..2c31138 100644 (file)
@@ -33,6 +33,7 @@ import RnEnv
 import RnSource   ( addTcgDUs )
 import HscTypes
 
+import Id( idType )
 import Class
 import Type
 import ErrUtils
@@ -323,7 +324,7 @@ tcDeriving tycl_decls inst_decls deriv_decls
         -- the stand-alone derived instances (@insts1@) are used when inferring
         -- the contexts for "deriving" clauses' instances (@infer_specs@)
         ; final_specs <- extendLocalInstEnv (map (iSpec . fst) insts1) $
-                           inferInstanceContexts overlap_flag infer_specs
+                         inferInstanceContexts overlap_flag infer_specs
 
         ; insts2 <- mapM (genInst False overlap_flag commonAuxs) final_specs
 
@@ -426,12 +427,11 @@ renameDeriv is_boot inst_infos bagBinds
                 -- scope (yuk), and rename the method binds
            ASSERT( null sigs )
            bindLocalNames (map Var.varName tyvars) $
-           do { (rn_binds, fvs) <- rnMethodBinds clas_nm (\_ -> []) binds
+           do { (rn_binds, fvs) <- rnMethodBinds (is_cls_nm inst) (\_ -> []) binds
               ; let binds' = VanillaInst rn_binds [] standalone_deriv
               ; return (inst_info { iBinds = binds' }, fvs) }
         where
-          (tyvars,_, clas,_) = instanceHead inst
-          clas_nm            = className clas
+          (tyvars, _) = tcSplitForAllTys (idType (instanceDFunId inst))
 \end{code}
 
 Note [Newtype deriving and unused constructors]
@@ -1378,8 +1378,7 @@ inferInstanceContexts oflag infer_specs
       | otherwise
       = do {      -- Extend the inst info from the explicit instance decls
                   -- with the current set of solutions, and simplify each RHS
-             let inst_specs = zipWithEqual "add_solns" (mkInstance oflag)
-                                           current_solns infer_specs
+             inst_specs <- zipWithM (mkInstance oflag) current_solns infer_specs
            ; new_solns <- checkNoErrs $
                           extendLocalInstEnv inst_specs $
                           mapM gen_soln infer_specs
@@ -1413,13 +1412,14 @@ inferInstanceContexts oflag infer_specs
         the_pred = mkClassPred clas inst_tys
 
 ------------------------------------------------------------------
-mkInstance :: OverlapFlag -> ThetaType -> DerivSpec -> ClsInst
+mkInstance :: OverlapFlag -> ThetaType -> DerivSpec -> TcM ClsInst
 mkInstance overlap_flag theta
-            (DS { ds_name = dfun_name
-                , ds_tvs = tyvars, ds_cls = clas, ds_tys = tys })
-  = mkLocalInstance dfun overlap_flag
+           (DS { ds_name = dfun_name
+               , ds_tvs = tvs, ds_cls = clas, ds_tys = tys })
+  = do { (subst, tvs') <- tcInstSkolTyVars tvs
+       ; return (mkLocalInstance dfun overlap_flag tvs' clas (substTys subst tys)) }
   where
-    dfun = mkDictFunId dfun_name tyvars theta clas tys
+    dfun = mkDictFunId dfun_name tvs theta clas tys
 
 
 extendLocalInstEnv :: [ClsInst] -> TcM a -> TcM a
@@ -1512,21 +1512,21 @@ genInst standalone_deriv oflag comauxs
                  , ds_theta = theta, ds_newtype = is_newtype
                  , ds_name = name, ds_cls = clas })
   | is_newtype
-  = return (InstInfo { iSpec   = inst_spec
-                     , iBinds  = NewTypeDerived co rep_tycon }, emptyBag)
+  = do { inst_spec <- mkInstance oflag theta spec
+       ; return (InstInfo { iSpec   = inst_spec
+                          , iBinds  = NewTypeDerived co rep_tycon }, emptyBag) }
 
   | otherwise
   = do { fix_env <- getFixityEnv
        ; (meth_binds, deriv_stuff) <- genDerivStuff (getSrcSpan name)
                                         fix_env clas name rep_tycon
                                         (lookup rep_tycon comauxs)
+       ; inst_spec <- mkInstance oflag theta spec
        ; let inst_info = InstInfo { iSpec   = inst_spec
                                   , iBinds  = VanillaInst meth_binds []
                                                 standalone_deriv }
        ; return ( inst_info, deriv_stuff) }
   where
-
-    inst_spec = mkInstance oflag theta spec
     co1 = case tyConFamilyCoercion_maybe rep_tycon of
               Just co_con -> mkTcUnbranchedAxInstCo co_con rep_tc_args
               Nothing     -> id_co
index 3a5cda3..528c06c 100644 (file)
@@ -700,7 +700,7 @@ pprInstInfoDetails info
 
 simpleInstInfoClsTy :: InstInfo a -> (Class, Type)
 simpleInstInfoClsTy info = case instanceHead (iSpec info) of
-                           (_, _, cls, [ty]) -> (cls, ty)
+                           (_, cls, [ty]) -> (cls, ty)
                            _ -> panic "simpleInstInfoClsTy"
 
 simpleInstInfoTy :: InstInfo a -> Type
index 3941017..7ed66bf 100644 (file)
@@ -136,33 +136,32 @@ metaTyConsToDerivStuff tc metaDts =
       let
         safeOverlap = safeLanguageOn dflags
         (dBinds,cBinds,sBinds) = mkBindsMetaD fix_env tc
+        mk_inst clas tc dfun_name 
+          = mkLocalInstance (mkDictFunId dfun_name [] [] clas tys)
+                            (NoOverlap safeOverlap)
+                            [] clas tys
+          where
+            tys = [mkTyConTy tc]
         
         -- Datatype
         d_metaTycon = metaD metaDts
-        d_inst = mkLocalInstance d_dfun $ NoOverlap safeOverlap
-        d_binds = VanillaInst dBinds [] False
-        d_dfun  = mkDictFunId d_dfun_name (tyConTyVars tc) [] dClas 
-                    [ mkTyConTy d_metaTycon ]
+        d_inst   = mk_inst dClas d_metaTycon d_dfun_name
+        d_binds  = VanillaInst dBinds [] False
         d_mkInst = DerivInst (InstInfo { iSpec = d_inst, iBinds = d_binds })
         
         -- Constructor
         c_metaTycons = metaC metaDts
-        c_insts = [ mkLocalInstance (c_dfun c ds) $ NoOverlap safeOverlap
+        c_insts = [ mk_inst cClas c ds
                   | (c, ds) <- myZip1 c_metaTycons c_dfun_names ]
         c_binds = [ VanillaInst c [] False | c <- cBinds ]
-        c_dfun c dfun_name = mkDictFunId dfun_name (tyConTyVars tc) [] cClas 
-                               [ mkTyConTy c ]
         c_mkInst = [ DerivInst (InstInfo { iSpec = is, iBinds = bs })
                    | (is,bs) <- myZip1 c_insts c_binds ]
         
         -- Selector
         s_metaTycons = metaS metaDts
-        s_insts = map (map (\(s,ds) -> mkLocalInstance (s_dfun s ds) $
-                                                  NoOverlap safeOverlap))
-                    (myZip2 s_metaTycons s_dfun_names)
+        s_insts = map (map (\(s,ds) -> mk_inst sClas s ds))
+                      (myZip2 s_metaTycons s_dfun_names)
         s_binds = [ [ VanillaInst s [] False | s <- ss ] | ss <- sBinds ]
-        s_dfun s dfun_name = mkDictFunId dfun_name (tyConTyVars tc) [] sClas
-                               [ mkTyConTy s ]
         s_mkInst = map (map (\(is,bs) -> DerivInst (InstInfo { iSpec  = is
                                                              , iBinds = bs})))
                        (myZip2 s_insts s_binds)
index bd6798b..a903d34 100644 (file)
@@ -421,7 +421,7 @@ tcInstDecls1 tycl_decls inst_decls deriv_decls
                 , deriv_binds)
     }}
   where
-    typInstCheck ty = is_cls (iSpec ty) `elem` typeableClassNames
+    typInstCheck ty = is_cls_nm (iSpec ty) `elem` typeableClassNames
     typInstErr = ptext $ sLit $ "Can't create hand written instances of Typeable in Safe"
                               ++ " Haskell! Can only derive them"
 
@@ -550,8 +550,11 @@ tcClsInstDecl (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds
                 -- Dfun location is that of instance *header*
 
         ; overlap_flag <- getOverlapFlag
+        ; (subst, tyvars') <- tcInstSkolTyVars tyvars
         ; let dfun     = mkDictFunId dfun_name tyvars theta clas inst_tys
-              ispec    = mkLocalInstance dfun overlap_flag
+              ispec    = mkLocalInstance dfun overlap_flag tyvars' clas (substTys subst inst_tys)
+                            -- Be sure to freshen those type variables, 
+                            -- so they are sure not to appear in any lookup
               inst_info = InstInfo { iSpec  = ispec, iBinds = VanillaInst binds uprags False }
 
         ; return ( [inst_info], tyfam_insts0 ++ concat tyfam_insts1 ++ datafam_insts) }
index 8e67b4f..0a25a6c 100644 (file)
@@ -1308,8 +1308,9 @@ reifyClassInstance i
        ; let head_ty = foldl TH.AppT (TH.ConT (reifyName cls)) thtypes
        ; return $ (TH.InstanceD cxt head_ty []) }
   where
-     (_tvs, theta, cls, types) = instanceHead i
-     n_silent = dfunNSilent (instanceDFunId i)
+     (_tvs, theta, cls, types) = tcSplitDFunTy (idType dfun)
+     dfun     = instanceDFunId i
+     n_silent = dfunNSilent dfun
 
 ------------------------------
 reifyFamilyInstance :: FamInst br -> TcM TH.Dec
index 8c8cb9a..ba2fa0d 100644 (file)
@@ -1096,23 +1096,20 @@ tcIsTyVarTy :: Type -> Bool
 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
 
 -----------------------
-tcSplitDFunTy :: Type -> ([TyVar], Int, Class, [Type])
+tcSplitDFunTy :: Type -> ([TyVar], [Type], Class, [Type])
 -- Split the type of a dictionary function
 -- We don't use tcSplitSigmaTy,  because a DFun may (with NDP)
 -- have non-Pred arguments, such as
 --     df :: forall m. (forall b. Eq b => Eq (m b)) -> C m
+-- 
+-- Also NB splitFunTys, not tcSplitFunTys; 
+-- the latter  specifically stops at PredTy arguments, 
+-- and we don't want to do that here
 tcSplitDFunTy ty 
-  = case tcSplitForAllTys ty   of { (tvs, rho)  ->
-    case split_dfun_args 0 rho of { (n_theta, tau) ->
-    case tcSplitDFunHead tau   of { (clas, tys) ->
-    (tvs, n_theta, clas, tys) }}}
-  where
-    -- Count the context of the dfun.  This can be a mix of
-    -- coercion and class constraints; or (in the general NDP case)
-    -- some other function argument
-    split_dfun_args n ty | Just ty' <- tcView ty = split_dfun_args n ty'
-    split_dfun_args n (FunTy _ ty)     = split_dfun_args (n+1) ty
-    split_dfun_args n ty               = (n, ty)
+  = case tcSplitForAllTys ty   of { (tvs, rho)   ->
+    case splitFunTys rho       of { (theta, tau) ->  
+    case tcSplitDFunHead tau   of { (clas, tys)  ->
+    (tvs, theta, clas, tys) }}}
 
 tcSplitDFunHead :: Type -> (Class, [Type])
 tcSplitDFunHead = getClassPredTys
index ab1007f..09d0be0 100644 (file)
@@ -28,9 +28,7 @@ module FunDeps (
 import Name
 import Var
 import Class
-import Id( idType )
 import Type
-import TcType( tcSplitDFunTy )
 import Unify
 import InstEnv
 import VarSet
@@ -348,7 +346,7 @@ checkClsFD :: FunDep TyVar -> [TyVar]                 -- One functional dependency fr
           -> [([TyVar], [FDEq])]
 
 checkClsFD fd clas_tvs 
-           (ClsInst { is_tvs = qtvs, is_tys = tys_inst, is_tcs = rough_tcs_inst, is_dfun = dfun })
+           (ClsInst { is_tvs = qtvs, is_tys = tys_inst, is_tcs = rough_tcs_inst })
            extra_qtvs tys_actual rough_tcs_actual
 
 -- 'qtvs' are the quantified type variables, the ones which an be instantiated 
@@ -420,9 +418,8 @@ checkClsFD fd clas_tvs
                         -- eqType again, since we know for sure that /at least one/ 
                         -- equation in there is useful)
 
-                    (dfun_tvs, _, _, _) = tcSplitDFunTy (idType dfun)
                    meta_tvs = [ setVarType tv (substTy subst (varType tv))
-                               | tv <- dfun_tvs, tv `notElemTvSubst` subst ]
+                               | tv <- qtvs, tv `notElemTvSubst` subst ]
                        -- meta_tvs are the quantified type variables
                        -- that have not been substituted out
                        --      
@@ -440,7 +437,8 @@ checkClsFD fd clas_tvs
                         --              whose kind mentions that kind variable!
                         --          Trac #6015, #6068
   where
-    bind_fn tv | tv `elemVarSet` qtvs       = BindMe
+    qtv_set = mkVarSet qtvs
+    bind_fn tv | tv `elemVarSet` qtv_set    = BindMe
                | tv `elemVarSet` extra_qtvs = BindMe
               | otherwise                  = Skolem
 
@@ -539,7 +537,7 @@ checkFunDeps inst_envs ispec
   | null bad_fundeps = Nothing
   | otherwise       = Just bad_fundeps
   where
-    (ins_tvs, _, clas, ins_tys) = instanceHead ispec
+    (ins_tvs, clas, ins_tys) = instanceHead ispec
     ins_tv_set   = mkVarSet ins_tvs
     cls_inst_env = classInstances inst_envs clas
     bad_fundeps  = badFunDeps cls_inst_env clas ins_tv_set ins_tys
index f99b0a1..dbfbc43 100644 (file)
@@ -10,8 +10,8 @@ The bits common to TcInstDcls and TcDeriv.
 module InstEnv (
         DFunId, OverlapFlag(..), InstMatch, ClsInstLookupResult,
         ClsInst(..), DFunInstType, pprInstance, pprInstanceHdr, pprInstances, 
-        instanceHead, mkLocalInstance, mkImportedInstance,
-        instanceDFunId, setInstanceDFunId, instanceRoughTcs,
+        instanceHead, instanceSig, mkLocalInstance, mkImportedInstance,
+        instanceDFunId, tidyClsInstDFun, instanceRoughTcs,
 
         InstEnv, emptyInstEnv, extendInstEnv, overwriteInstEnv, 
         extendInstEnvList, lookupUniqueInstEnv, lookupInstEnv', lookupInstEnv, instEnvElts,
@@ -48,17 +48,19 @@ import Data.Maybe       ( isJust, isNothing )
 
 \begin{code}
 data ClsInst 
-  = ClsInst { is_cls  :: Name  -- Class name
-
-                -- Used for "rough matching"; see Note [Rough-match field]
+  = ClsInst {   -- Used for "rough matching"; see Note [Rough-match field]
                 -- INVARIANT: is_tcs = roughMatchTcs is_tys
+               is_cls_nm :: Name  -- Class name
              , is_tcs  :: [Maybe Name]  -- Top of type args
 
                 -- Used for "proper matching"; see Note [Proper-match fields]
-             , is_tvs  :: TyVarSet      -- Template tyvars for full match
-             , is_tys  :: [Type]        -- Full arg types
+             , is_tvs  :: [TyVar]       -- Fresh template tyvars for full match
+                                        -- See Note [Template tyvars are fresh]
+             , is_cls  :: Class         -- The real class
+             , is_tys  :: [Type]        -- Full arg types (mentioning is_tvs)
                 -- INVARIANT: is_dfun Id has type 
                 --      forall is_tvs. (...) => is_cls is_tys
+                -- (modulo alpha conversion)
 
              , is_dfun :: DFunId -- See Note [Haddock assumptions]
                     -- See Note [Silent superclass arguments] in TcInstDcls
@@ -71,10 +73,22 @@ data ClsInst
   deriving (Data, Typeable)
 \end{code}
 
+Note [Template tyvars are fresh]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The is_tvs field of a ClsInst has *completely fresh* tyvars.  
+That is, they are
+  * distinct from any other ClsInst
+  * distinct from any tyvars free in predicates that may
+    be looked up in the class instance environment
+Reason for freshness: we use unification when checking for overlap
+etc, and that requires the tyvars to be distinct.
+
+The invariant is checked by the ASSERT in lookupInstEnv'.
+
 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
+The is_cls_nm, 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
@@ -92,18 +106,17 @@ In is_tcs,
 
 Note [Proper-match fields]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
-The is_tvs, is_tys fields are simply cached values, pulled
+The is_tvs, is_cls, 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
+that we often never poke the 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.)
+ * is_tvs, is_tys may be alpha-renamed compared to the ones in
+   the dfun Id
 
 Note [Haddock assumptions]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -124,19 +137,9 @@ being equal to
 instanceDFunId :: ClsInst -> DFunId
 instanceDFunId = is_dfun
 
-setInstanceDFunId :: ClsInst -> DFunId -> ClsInst
-setInstanceDFunId ispec dfun
-   = ASSERT2( idType dfun `eqType` idType (is_dfun ispec)
-            , ppr dfun $$ ppr (idType dfun) $$ ppr (is_dfun ispec) $$ ppr (idType (is_dfun ispec)) )
-        -- We need to create the cached fields afresh from
-        -- the new dfun id.  In particular, the is_tvs in
-        -- the ClsInst must match those in the dfun!
-        -- We assume that the only thing that changes is
-        -- the quantified type variables, so the other fields
-        -- are ok; hence the assert
-     ispec { is_dfun = dfun, is_tvs = mkVarSet tvs, is_tys = tys }
-   where 
-     (tvs, _, _, tys) = tcSplitDFunTy (idType dfun)
+tidyClsInstDFun :: (DFunId -> DFunId) -> ClsInst -> ClsInst
+tidyClsInstDFun tidy_dfun ispec
+  = ispec { is_dfun = tidy_dfun (is_dfun ispec) }
 
 instanceRoughTcs :: ClsInst -> [Maybe Name]
 instanceRoughTcs = is_tcs
@@ -173,34 +176,39 @@ pprInstanceHdr (ClsInst { is_flag = flag, is_dfun = dfun })
 pprInstances :: [ClsInst] -> SDoc
 pprInstances ispecs = vcat (map pprInstance ispecs)
 
-instanceHead :: ClsInst -> ([TyVar], ThetaType, Class, [Type])
-instanceHead ispec = (tvs, theta, cls, tys)
+instanceHead :: ClsInst -> ([TyVar], Class, [Type])
+-- Returns the head, using the fresh tyavs from the ClsInst
+instanceHead (ClsInst { is_tvs = tvs, is_tys = tys, is_dfun = dfun })
+   = (tvs, cls, tys)
    where
-     (tvs, theta, tau) = tcSplitSigmaTy (idType dfun)
-     (cls, tys)        = tcSplitDFunHead tau
-     dfun              = is_dfun ispec
+     (_, _, cls, _) = tcSplitDFunTy (idType dfun)
+
+instanceSig :: ClsInst -> ([TyVar], [Type], Class, [Type])
+-- Decomposes the DFunId
+instanceSig ispec = tcSplitDFunTy (idType (is_dfun ispec))
 
-mkLocalInstance :: DFunId
-                -> OverlapFlag
+mkLocalInstance :: DFunId -> OverlapFlag
+                -> [TyVar] -> Class -> [Type]
                 -> ClsInst
 -- Used for local instances, where we can safely pull on the DFunId
-mkLocalInstance dfun oflag
-  = ClsInst {  is_flag = oflag, is_dfun = dfun,
-                is_tvs = mkVarSet tvs, is_tys = tys,
-                is_cls = className cls, is_tcs = roughMatchTcs tys }
-  where
-    (tvs, _, cls, tys) = tcSplitDFunTy (idType dfun)
+mkLocalInstance dfun oflag tvs cls tys
+  = ClsInst { is_flag = oflag, is_dfun = dfun
+            , is_tvs = tvs
+            , is_cls = cls, is_cls_nm = className cls
+            , is_tys = tys, is_tcs = roughMatchTcs tys }
 
 mkImportedInstance :: Name -> [Maybe Name]
                    -> DFunId -> OverlapFlag -> ClsInst
 -- Used for imported instances, where we get the rough-match stuff
 -- from the interface file
-mkImportedInstance cls mb_tcs dfun oflag
-  = ClsInst {  is_flag = oflag, is_dfun = dfun,
-                is_tvs = mkVarSet tvs, is_tys = tys,
-                is_cls = cls, is_tcs = mb_tcs }
+-- The bound tyvars of the dfun are guaranteed fresh, because
+-- the dfun has been typechecked out of the same interface file
+mkImportedInstance cls_nm mb_tcs dfun oflag
+  = ClsInst { is_flag = oflag, is_dfun = dfun
+            , is_tvs = tvs, is_tys = tys
+            , is_cls_nm = cls_nm, is_cls = cls, is_tcs = mb_tcs }
   where
-    (tvs, _, _, tys) = tcSplitDFunTy (idType dfun)
+    (tvs, _, cls, tys) = tcSplitDFunTy (idType dfun)
 
 roughMatchTcs :: [Type] -> [Maybe Name]
 roughMatchTcs tys = map rough tys
@@ -395,30 +403,28 @@ extendInstEnvList :: InstEnv -> [ClsInst] -> InstEnv
 extendInstEnvList inst_env ispecs = foldl extendInstEnv inst_env ispecs
 
 extendInstEnv :: InstEnv -> ClsInst -> InstEnv
-extendInstEnv inst_env ins_item@(ClsInst { is_cls = cls_nm })
+extendInstEnv inst_env ins_item@(ClsInst { is_cls_nm = cls_nm })
   = addToUFM_C add inst_env cls_nm (ClsIE [ins_item])
   where
     add (ClsIE cur_insts) _ = ClsIE (ins_item : cur_insts)
 
 overwriteInstEnv :: InstEnv -> ClsInst -> InstEnv
-overwriteInstEnv inst_env ins_item@(ClsInst { is_cls = cls_nm, is_tys = tys })
+overwriteInstEnv inst_env ins_item@(ClsInst { is_cls_nm = cls_nm, is_tys = tys })
   = addToUFM_C add inst_env cls_nm (ClsIE [ins_item])
   where
     add (ClsIE cur_insts) _ = ClsIE (replaceInst cur_insts)
     
     rough_tcs  = roughMatchTcs tys
     replaceInst [] = [ins_item]
-    replaceInst (item@(ClsInst { is_tcs = mb_tcs,  is_tvs = tpl_tvs, 
-                                  is_tys = tpl_tys,
-                                  is_dfun = dfun }) : rest)
+    replaceInst (item@(ClsInst { is_tcs = mb_tcs,  is_tvs = tpl_tvs 
+                               , is_tys = tpl_tys }) : rest)
     -- Fast check for no match, uses the "rough match" fields
       | instanceCantMatch rough_tcs mb_tcs
       = item : replaceInst rest
 
-      | Just _ <- tcMatchTys tpl_tvs tpl_tys tys
-      = let (dfun_tvs, _) = tcSplitForAllTys (idType dfun)
-        in ASSERT( all (`elemVarSet` tpl_tvs) dfun_tvs )        -- Check invariant
-           ins_item : rest
+      | let tpl_tv_set = mkVarSet tpl_tvs
+      , Just _ <- tcMatchTys tpl_tv_set tpl_tys tys
+      = ins_item : rest
 
       | otherwise
       = item : replaceInst rest
@@ -508,19 +514,14 @@ lookupInstEnv' ie cls tys
 
     --------------
     find ms us [] = (ms, us)
-    find ms us (item@(ClsInst { is_tcs = mb_tcs, is_tvs = tpl_tvs, 
-                                 is_tys = tpl_tys, is_flag = oflag,
-                                 is_dfun = dfun }) : rest)
+    find ms us (item@(ClsInst { is_tcs = mb_tcs, is_tvs = tpl_tvs
+                              , is_tys = tpl_tys, is_flag = oflag }) : rest)
         -- Fast check for no match, uses the "rough match" fields
       | instanceCantMatch rough_tcs mb_tcs
       = find ms us rest
 
-      | Just subst <- tcMatchTys tpl_tvs tpl_tys tys
-      = 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
+      | Just subst <- tcMatchTys tpl_tv_set tpl_tys tys
+      = find ((item, map (lookup_tv subst) tpl_tvs) : ms) us rest
 
         -- Does not match, so next check whether the things unify
         -- See Note [Overlapping instances] above
@@ -528,15 +529,18 @@ lookupInstEnv' ie cls tys
       = find ms us rest
 
       | otherwise
-      = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tvs,
+      = ASSERT2( tyVarsOfTypes tys `disjointVarSet` tpl_tv_set,
                  (ppr cls <+> ppr tys <+> ppr all_tvs) $$
-                 (ppr dfun <+> ppr tpl_tvs <+> ppr tpl_tys)
+                 (ppr tpl_tvs <+> ppr tpl_tys)
                 )
                 -- Unification will break badly if the variables overlap
                 -- They shouldn't because we allocate separate uniques for them
+                -- See Note [Template tyvars are fresh]
         case tcUnifyTys instanceBindFun tpl_tys tys of
             Just _   -> find ms (item:us) rest
             Nothing  -> find ms us        rest
+      where
+        tpl_tv_set = mkVarSet tpl_tvs
 
     ----------------
     lookup_tv :: TvSubst -> TyVar -> DFunInstType
@@ -616,7 +620,7 @@ insert_overlapping new_item (item:items)
 
     (instA, _) `beats` (instB, _)
           = overlap_ok && 
-            isJust (tcMatchTys (is_tvs instB) (is_tys instB) (is_tys instA))
+            isJust (tcMatchTys (mkVarSet (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