(F)SLIT -> (f)sLit in TcTyFuns
[ghc-hetmet.git] / compiler / typecheck / TcTyFuns.lhs
index 126a029..4c5be1c 100644 (file)
@@ -7,11 +7,9 @@ module TcTyFuns (
 
        normaliseGivenEqs, normaliseGivenDicts, 
        normaliseWantedEqs, normaliseWantedDicts,
-       solveWantedEqs,
-       substEqInDictInsts,
        
         -- errors
-        eqInstMisMatch, misMatchMsg,
+        misMatchMsg, failWithMisMatch
   ) where
 
 
@@ -37,10 +35,11 @@ import Bag
 import Outputable
 import SrcLoc  ( Located(..) )
 import Maybes
+import FastString
 
 -- standard
 import Data.List
-import Control.Monad (liftM)
+import Control.Monad
 \end{code}
 
 
@@ -99,27 +98,80 @@ tcNormaliseFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType)
 tcNormaliseFamInstPred = tcGenericNormaliseFamInstPred tcUnfoldSynFamInst
 \end{code}
 
-Normalise a type relative to the rewrite rule implied by one EqInst or an
-already unpacked EqInst (ie, an equality rewrite rule).
+An elementary rewrite is a properly oriented equality with associated coercion
+that has one of the following two forms:
+
+(1) co :: F t1..tn ~ t
+(2) co :: a ~ t         , where t /= F t1..tn and a is a skolem tyvar
+
+NB: We do *not* use equalities of the form a ~ t where a is a meta tyvar as a
+reqrite rule.  Instead, such equalities are solved by unification.  This is
+essential; cf Note [skolemOccurs loop].
+
+The following functions takes an equality instance and turns it into an
+elementary rewrite if possible.
 
 \begin{code}
--- Rewrite by EqInst
-tcEqInstNormaliseFamInst :: Inst -> TcType -> TcM (CoercionI, Type)
-tcEqInstNormaliseFamInst inst = 
-  ASSERT( isEqInst inst )
-  tcEqRuleNormaliseFamInst (pat, rhs, co)
+data Rewrite = Rewrite TcType           -- lhs of rewrite rule
+                       TcType           -- rhs of rewrite rule
+                       TcType           -- coercion witnessing the rewrite rule
+
+eqInstToRewrite :: Inst -> Maybe (Rewrite, Bool)
+                                           -- True iff rewrite swapped equality
+eqInstToRewrite inst
+  = ASSERT( isEqInst inst )
+    go ty1 ty2 (eqInstType inst)
   where
-    pat = eqInstLeftTy  inst
-    rhs = eqInstRightTy inst
-    co  = eqInstType    inst
+    (ty1,ty2) = eqInstTys inst
+
+    -- look through synonyms
+    go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
+    go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
+
+    -- left-to-right rule with type family head
+    go ty1@(TyConApp con _) ty2 co 
+      | isOpenSynTyCon con
+      = Just (Rewrite ty1 ty2 co, False)                     -- not swapped
+
+    -- left-to-right rule with type variable head
+    go ty1@(TyVarTy tv) ty2 co 
+      | isSkolemTyVar tv
+      = Just (Rewrite ty1 ty2 co, False)                     -- not swapped
+
+    -- right-to-left rule with type family head, only after
+    -- having checked whether we can work left-to-right
+    go ty1 ty2@(TyConApp con _) co 
+      | isOpenSynTyCon con
+      = Just (Rewrite ty2 ty1 (mkSymCoercion co), True)      -- swapped
+
+    -- right-to-left rule with type variable head, only after 
+    -- having checked whether we can work left-to-right 
+    go ty1 ty2@(TyVarTy tv) co 
+      | isSkolemTyVar tv
+      = Just (Rewrite ty2 ty1 (mkSymCoercion co), True)      -- swapped
+
+    -- this equality is not a rewrite rule => ignore
+    go _ _ _ = Nothing
+\end{code}
+
+Normalise a type relative to an elementary rewrite implied by an EqInst or an
+explicitly given elementary rewrite.
+
+\begin{code}
+-- Rewrite by EqInst
+--   Precondition: the EqInst passes the occurs check
+tcEqInstNormaliseFamInst :: Inst -> TcType -> TcM (CoercionI, TcType)
+tcEqInstNormaliseFamInst inst ty
+  = case eqInstToRewrite inst of
+      Just (rewrite, _) -> tcEqRuleNormaliseFamInst rewrite ty
+      Nothing           -> return (IdCo, ty)
 
 -- Rewrite by equality rewrite rule
-tcEqRuleNormaliseFamInst :: (TcType,   -- rewrite rule lhs
-                             TcType,   -- rewrite rule rhs
-                             TcType)   -- coercion witnessing the rewrite rule
-                          -> TcType    -- type to rewrite
-                          -> TcM (CoercionI, Type)
-tcEqRuleNormaliseFamInst (pat, rhs, co) ty
+tcEqRuleNormaliseFamInst :: Rewrite                     -- elementary rewrite
+                         -> TcType                      -- type to rewrite
+                         -> TcM (CoercionI,             -- witnessing coercion
+                                 TcType)                -- rewritten type
+tcEqRuleNormaliseFamInst (Rewrite pat rhs co) ty
   = tcGenericNormaliseFamInst matchEqRule ty
   where
     matchEqRule sty | pat `tcEqType` sty = return $ Just (rhs, co)
@@ -178,10 +230,6 @@ tcGenericNormaliseFamInst fun (ForAllTy tyvar ty1)
   = do         { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
        ; return (mkForAllTyCoI tyvar coi, mkForAllTy tyvar nty1)
        }
-tcGenericNormaliseFamInst fun (NoteTy note ty1)
-  = do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
-       ; return (mkNoteTyCoI note coi, NoteTy note nty1)
-       }
 tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
   | isTcTyVar tv
   = do { traceTc (text "tcGenericNormaliseFamInst" <+> ppr ty)
@@ -258,38 +306,12 @@ normaliseGivenEqs givens
 \end{code}
 
 \begin{code}
-normaliseWantedEqs :: [Inst] -> TcM [Inst]
-normaliseWantedEqs insts 
-  = do { traceTc (text "normaliseWantedEqs <-" <+> ppr insts)
-       ; result <- liftM fst $ rewriteToFixedPoint Nothing
-                    [ ("(ZONK)",    dontRerun $ zonkInsts)
-                    , ("(TRIVIAL)", dontRerun $ trivialRule)
-                    , ("(DECOMP)",  decompRule)
-                    , ("(TOP)",     topRule)
-                    , ("(UNIFY)",   unifyMetaRule)      -- incl. occurs check
-                    , ("(SUBST)",   substRule)          -- incl. occurs check
-                     ] insts
-       ; traceTc (text "normaliseWantedEqs ->" <+> ppr result)
-       ; return result
-       }
-\end{code}
-
-
-%************************************************************************
-%*                                                                     *
-\section{Solving of wanted constraints with respect to a given set}
-%*                                                                     *
-%************************************************************************
-
-The set of given equalities must have been normalised already.
-
-\begin{code}
-solveWantedEqs :: [Inst]        -- givens
-            -> [Inst]          -- wanteds
-            -> TcM [Inst]      -- irreducible wanteds
-solveWantedEqs givens wanteds 
-  = do { traceTc $ text "solveWantedEqs <-" <+> ppr wanteds <+> text "with" <+> 
-                   ppr givens
+normaliseWantedEqs :: [Inst]        -- givens
+                  -> [Inst]        -- wanteds
+                  -> TcM [Inst]    -- irreducible wanteds
+normaliseWantedEqs givens wanteds 
+  = do { traceTc $ text "normaliseWantedEqs <-" <+> ppr wanteds 
+                   <+> text "with" <+> ppr givens
        ; result <- liftM fst $ rewriteToFixedPoint Nothing
                      [ ("(ZONK)",    dontRerun $ zonkInsts)
                      , ("(TRIVIAL)", dontRerun $ trivialRule)
@@ -297,8 +319,9 @@ solveWantedEqs givens wanteds
                      , ("(TOP)",     topRule)
                      , ("(GIVEN)",   substGivens givens) -- incl. occurs check
                      , ("(UNIFY)",   unifyMetaRule)      -- incl. occurs check
+                    , ("(SUBST)",   substRule)          -- incl. occurs check
                      ] wanteds
-       ; traceTc (text "solveWantedEqs ->" <+> ppr result)
+       ; traceTc (text "normaliseWantedEqs ->" <+> ppr result)
        ; return result
        }
   where
@@ -335,14 +358,18 @@ normalise_dicts
                        -- Fals <=> they are given
        -> TcM ([Inst],TcDictBinds)
 normalise_dicts given_eqs dicts is_wanted
-  = do { traceTc $ text "normalise???Dicts <-" <+> ppr dicts <+> 
+  = do { traceTc $ let name | is_wanted = "normaliseWantedDicts <-"
+                             | otherwise = "normaliseGivenDicts <-"
+                    in
+                    text name <+> ppr dicts <+> 
                     text "with" <+> ppr given_eqs
        ; (dicts0, binds0)  <- normaliseInsts is_wanted dicts
-       ; (dicts1, binds1)  <- substEqInDictInsts given_eqs dicts0
+       ; (dicts1, binds1)  <- substEqInDictInsts is_wanted given_eqs dicts0
        ; let binds01 = binds0 `unionBags` binds1
        ; if isEmptyBag binds1
          then return (dicts1, binds01)
-         else do { (dicts2, binds2) <- normaliseGivenDicts given_eqs dicts1
+         else do { (dicts2, binds2) <- 
+                      normalise_dicts given_eqs dicts1 is_wanted
                  ; return (dicts2, binds01 `unionBags` binds2) } }
 \end{code}
 
@@ -444,7 +471,7 @@ oriented properly, like
 
      F a ~ [G (F a)]
  or even
-     a ~ [G a]
+     a ~ [G a]          , where a is a skolem tyvar
 
 The left-to-right orientiation is not suitable because it does not
 terminate. The right-to-left orientation is not suitable because it 
@@ -489,6 +516,45 @@ NB: We perform this transformation for multiple occurences of ty1 under one
     rule doesn't need to be applied multiple times at a single inst).  As a 
     result we can get two or more insts back.
 
+Note [skolemOccurs loop]
+~~~~~~~~~~~~~~~~~~~~~~~~
+You might think that under
+
+  type family F a 
+  type instance F [a] = [F a]
+
+a signature such as
+
+  foo :: (F [a] ~ a) => a
+
+will get us into a loop.  However, this is *not* the case.  Here is why:
+
+    F [a<sk>] ~ a<sk>
+
+    -->(TOP)
+
+    [F a<sk>] ~ a<sk>
+
+    -->(SkolemOccurs)
+
+    [b<tau>] ~ a<sk>
+    F [b<tau>] ~ b<tau>   , with b := F a
+
+    -->(TOP)
+
+    [b<tau>] ~ a<sk>
+    [F b<tau>] ~ b<tau>   , with b := F a
+
+At this point (SkolemOccurs) does *not* apply anymore, as 
+
+  [F b<tau>] ~ b<tau>
+
+is not used as a rewrite rule.  The variable b<tau> is not a skolem (cf
+eqInstToRewrite). 
+
+(The regression test indexed-types/should_compile/Simple20 checks that the
+described property of the system does not change.)
+
 \begin{code}
 skolemOccurs :: PrecondRule
 skolemOccurs insts
@@ -498,40 +564,24 @@ skolemOccurs insts
   where
     oneSkolemOccurs inst
       = ASSERT( isEqInst inst )
-        isRewriteRule (eqInstLeftTy inst) (eqInstRightTy inst)
+        case eqInstToRewrite inst of
+          Just (rewrite, swapped) -> breakRecursion rewrite swapped
+          Nothing                 -> return ([inst], return ())
       where
+        -- inst is an elementary rewrite rule, check whether we need to break
+        -- it up
+        breakRecursion (Rewrite pat body _) swapped
 
-        -- look through synonyms
-        isRewriteRule ty1 ty2 | Just ty1' <- tcView ty1 = isRewriteRule ty1' ty2
-        isRewriteRule ty1 ty2 | Just ty2' <- tcView ty2 = isRewriteRule ty1 ty2'
-
-        -- left-to-right rule with type family head
-        isRewriteRule ty1@(TyConApp con _) ty2
-          | isOpenSynTyCon con
-          = breakRecursion ty1 ty2 False    -- not swapped
-
-        -- left-to-right rule with type variable head
-        isRewriteRule ty1@(TyVarTy _) ty2
-          = breakRecursion ty1 ty2 False    -- not swapped
-
-        -- right-to-left rule with type family head
-        isRewriteRule ty1 ty2@(TyConApp con _)
-          | isOpenSynTyCon con
-          = breakRecursion ty2 ty1 True     -- swapped
-
-        -- right-to-left rule with type variable head
-        isRewriteRule ty1 ty2@(TyVarTy _)
-          = breakRecursion ty2 ty1 True     -- swapped
-
-        -- this equality is not a rewrite rule => ignore
-        isRewriteRule _ _ = return ([inst], return ())
-
-
-        breakRecursion pat body swapped
+          -- skolemOccurs does not apply, leave as is
           | null tysToLiftOut 
-          = return ([inst], return ())
+          = do { traceTc $ text "oneSkolemOccurs: no tys to lift out"
+               ; return ([inst], return ())
+               }
+
+          -- recursive occurence of pat in body under a type family application
           | otherwise
-          = do { skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut
+          = do { traceTc $ text "oneSkolemOccurs[TLO]:" <+> ppr tysToLiftOut
+               ; skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut
                ; let skTvs_tysTLO   = zip skTvs tysToLiftOut
                      insertSkolems = return . replace skTvs_tysTLO
                ; (_, body') <- tcGenericNormaliseFamInst insertSkolems body
@@ -539,6 +589,7 @@ skolemOccurs insts
                                      else mkEqInst (EqPred pat body') co
                                      -- ensure to reconstruct the inst in the
                                      -- original orientation
+               ; traceTc $ text "oneSkolemOccurs[inst']:" <+> ppr inst'
                ; (insts, undoSk) <- mapAndUnzipM (mkSkolemInst inst') 
                                                  skTvs_tysTLO
                ; return (inst':insts, sequence_ undoSk)
@@ -564,6 +615,7 @@ skolemOccurs insts
               = do { (co, tyLiftedOut) <- tcEqInstNormaliseFamInst inst' tyTLO
                    ; inst <- mkEqInst (EqPred tyLiftedOut (mkTyVarTy skTv)) 
                                       (mkGivenCo $ mkSymCoercion (fromACo co))
+                                      -- co /= IdCo due to construction of inst'
                    ; return (inst, writeMetaTyVar skTv tyTLO) 
                    }
 \end{code}
@@ -581,7 +633,7 @@ The following rules exploits the reflexivity of equality:
 \begin{code}
 trivialRule :: IdemRewriteRule
 trivialRule insts 
-  = liftM catMaybes $ mappM trivial insts
+  = liftM catMaybes $ mapM trivial insts
   where
     trivial inst
       | ASSERT( isEqInst inst )
@@ -594,8 +646,7 @@ trivialRule insts
       | otherwise
       = return $ Just inst
       where
-        ty1 = eqInstLeftTy  inst
-        ty2 = eqInstRightTy inst
+        (ty1,ty2) = eqInstTys inst
 \end{code}
 
 
@@ -626,8 +677,9 @@ decompRule insts
   where
     decomp inst
       = ASSERT( isEqInst inst )
-        go (eqInstLeftTy inst) (eqInstRightTy inst)
+        go ty1 ty2
       where
+       (ty1,ty2) = eqInstTys inst
         go ty1 ty2             
           | Just ty1' <- tcView ty1 = go ty1' ty2 
           | Just ty2' <- tcView ty2 = go ty1 ty2' 
@@ -746,8 +798,7 @@ topRule insts
                    }
             }
       where
-        ty1 = eqInstLeftTy  inst
-       ty2 = eqInstRightTy inst
+        (ty1,ty2) = eqInstTys inst
 \end{code}
 
 
@@ -799,43 +850,14 @@ substRule insts = tryAllInsts insts []
 --
 substInst :: Inst -> [Inst] -> TcM ([Inst], Bool)
 substInst inst insts
-  = ASSERT( isEqInst inst )
-    go (eqInstLeftTy inst) (eqInstRightTy inst) (eqInstType inst)
+  = case eqInstToRewrite inst of
+      Just (rewrite, _) -> substEquality rewrite insts
+      Nothing           -> return (insts, False)
   where
-    -- look through synonyms
-    go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
-    go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
-
-    -- rewrite type family applications
-    go ty1@(TyConApp con _) ty2 co 
-      | isOpenSynTyCon con
-      = substEquality (ty1, ty2, co) insts
-
-    -- rewrite skolems
-    go ty1@(TyVarTy tv) ty2 co 
-      | isSkolemTyVar tv
-      = substEquality (ty1, ty2, co) insts
-
-    -- rewrite type family applications from right-to-left, only after
-    -- having checked whether we can work left-to-right
-    go ty1 ty2@(TyConApp con _) co 
-      | isOpenSynTyCon con
-      = substEquality (ty2, ty1, mkSymCoercion co) insts
-
-    -- rewrite skolems from right-to-left, only after having checked
-    -- whether we can work left-to-right 
-    go ty1 ty2@(TyVarTy tv) co 
-      | isSkolemTyVar tv
-      = substEquality (ty2, ty1, mkSymCoercion co) insts
-
-    go _ _ _ = return (insts, False)
-
-    substEquality :: (TcType,   -- rewrite rule lhs
-                      TcType,   -- rewrite rule rhs
-                      TcType)   -- coercion witnessing the rewrite rule
-                  -> [Inst]     -- insts to rewrite
+    substEquality :: Rewrite            -- elementary rewrite
+                  -> [Inst]             -- insts to rewrite
                   -> TcM ([Inst], Bool)
-    substEquality eqRule@(pat, rhs, _) insts
+    substEquality eqRule@(Rewrite pat rhs _) insts
       | pat `tcPartOfType` rhs      -- occurs check!
       = occurCheckErr pat rhs
       | otherwise
@@ -874,8 +896,7 @@ substInst inst insts
                     }
               }
          where 
-            ty1 = eqInstLeftTy  inst
-            ty2 = eqInstRightTy inst
+            (ty1,ty2) = eqInstTys inst
 \end{code}
 
 
@@ -912,9 +933,10 @@ unifyMetaRule insts
   where
     unifyMeta inst
       = ASSERT( isEqInst inst )
-        go (eqInstLeftTy inst) (eqInstRightTy inst)
+        go ty1 ty2
            (fromWantedCo "unifyMetaRule" $ eqInstCoercion inst)
       where
+       (ty1,ty2) = eqInstTys inst
         go ty1 ty2 cotv
           | Just ty1' <- tcView ty1 = go ty1' ty2 cotv
           | Just ty2' <- tcView ty2 = go ty1 ty2' cotv
@@ -934,26 +956,30 @@ unifyMetaRule insts
         uMeta _swapped _tv (IndirectTv _) _ty _cotv
           = return ([inst], False)
 
-        -- signature skolem meets non-variable type
-        -- => cannot update!
-        uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) ty _cotv
-          | not $ isTyVarTy ty
-          = return ([inst], False)
-
         -- type variable meets type variable
         -- => check that tv2 hasn't been updated yet and choose which to update
        uMeta swapped tv1 (DoneTv details1) (TyVarTy tv2) cotv
+         | tv1 == tv2
+         = return ([inst], False)      -- The two types are already identical
+
+         | otherwise
          = do { lookupTV2 <- lookupTcTyVar tv2
                ; case lookupTV2 of
-                   IndirectTv ty  -> uMeta swapped tv1 (DoneTv details1) ty cotv
-                   DoneTv details2 -> 
-                     uMetaVar swapped tv1 details1 tv2 details2 cotv
+                   IndirectTv ty   -> uMeta swapped tv1 (DoneTv details1) ty cotv
+                   DoneTv details2 -> uMetaVar swapped tv1 details1 tv2 details2 cotv
               }
 
+       ------ Beyond this point we know that ty2 is not a type variable
+
+        -- signature skolem meets non-variable type
+        -- => cannot update!
+        uMeta _swapped _tv (DoneTv (MetaTv (SigTv _) _)) _non_tv_ty _cotv
+          = return ([inst], False)
+
         -- updatable meta variable meets non-variable type
         -- => occurs check, monotype check, and kinds match check, then update
-       uMeta swapped tv (DoneTv (MetaTv _ ref)) ty cotv
-         = do { mb_ty' <- checkTauTvUpdate tv ty    -- occurs + monotype check
+       uMeta swapped tv (DoneTv (MetaTv _ ref)) non_tv_ty cotv
+         = do { mb_ty' <- checkTauTvUpdate tv non_tv_ty    -- occurs + monotype check
                ; case mb_ty' of
                    Nothing  -> return ([inst], False)  -- tv occurs in faminst
                    Just ty' ->
@@ -965,6 +991,7 @@ unifyMetaRule insts
 
         uMeta _ _ _ _ _ = panic "uMeta"
 
+       -- uMetaVar: unify two type variables
         -- meta variable meets skolem 
         -- => just update
         uMetaVar swapped tv1 (MetaTv _ ref) tv2 (SkolemTv _) cotv
@@ -1032,10 +1059,11 @@ form
 where F is a type family.
 
 \begin{code}
-substEqInDictInsts :: [Inst]    -- given equalities (used as rewrite rules)
+substEqInDictInsts :: Bool      -- whether the *dictionaries* are wanted/given
+                   -> [Inst]    -- given equalities (used as rewrite rules)
                    -> [Inst]    -- dictinaries to be normalised
                    -> TcM ([Inst], TcDictBinds)
-substEqInDictInsts eqInsts dictInsts 
+substEqInDictInsts isWanted eqInsts dictInsts 
   = do { traceTc (text "substEqInDictInst <-" <+> ppr dictInsts)
        ; dictInsts' <- 
            foldlM rewriteWithOneEquality (dictInsts, emptyBag) eqInsts
@@ -1049,7 +1077,7 @@ substEqInDictInsts eqInsts dictInsts
                                            tci_right = target})
       | isOpenSynTyConApp pattern || isTyVarTy pattern
       = do { (dictInsts', moreDictBinds) <- 
-               genericNormaliseInsts True {- wanted -} applyThisEq dictInsts
+               genericNormaliseInsts isWanted applyThisEq dictInsts
            ; return (dictInsts', dictBinds `unionBags` moreDictBinds)
            }
       where
@@ -1124,11 +1152,17 @@ genericNormaliseInsts isWanted fun insts
                              --        else
                              --          dict' = dict  `cast` co
                          expr      = HsVar $ instToId source_dict
-                         cast_expr = HsWrap (WpCo st_co) expr
+                         cast_expr = HsWrap (WpCast st_co) expr
                          rhs       = L (instLocSpan loc) cast_expr
                          binds     = instToDictBind target_dict rhs
                      -- return the new inst
-                   ; traceTc $ text "genericNormaliseInst ->" <+> ppr dict'
+                   ; traceTc $ let name | isWanted 
+                                         = "genericNormaliseInst (wanted) ->"
+                                         | otherwise
+                                         = "genericNormaliseInst (given) ->"
+                                in
+                                text name <+> ppr dict' <+>
+                                text "with" <+> ppr binds
                     ; return (dict', binds)
                    }
           }
@@ -1136,6 +1170,8 @@ genericNormaliseInsts isWanted fun insts
        -- TOMDO: What do we have to do about ImplicInst, Method, and LitInst??
     normaliseOneInst _isWanted _fun inst
       = do { inst' <- zonkInst inst
+           ; traceTc $ text "*** TcTyFuns.normaliseOneInst: Skipping" <+>
+                       ppr inst
           ; return (inst', emptyBag)
           }
 \end{code}
@@ -1154,45 +1190,49 @@ somethingdifferent message.
 eqInstMisMatch :: Inst -> TcM a
 eqInstMisMatch inst
   = ASSERT( isEqInst inst )
-    do { (env, msg) <- misMatchMsg ty_act ty_exp
-       ; setErrCtxt ctxt $
-           failWithTcM (env, msg)
-       }
+    setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp
   where
-    ty_act           = eqInstLeftTy  inst
-    ty_exp           = eqInstRightTy inst
-    InstLoc _ _ ctxt = instLoc       inst
+    (ty_act, ty_exp) = eqInstTys inst
+    InstLoc _ _ ctxt = instLoc   inst
 
 -----------------------
-misMatchMsg :: TcType -> TcType -> TcM (TidyEnv, SDoc)
+failWithMisMatch :: TcType -> TcType -> TcM a
 -- Generate the message when two types fail to match,
 -- going to some trouble to make it helpful.
 -- The argument order is: actual type, expected type
-misMatchMsg ty_act ty_exp
+failWithMisMatch ty_act ty_exp
   = do { env0 <- tcInitTidyEnv
         ; ty_exp <- zonkTcType ty_exp
         ; ty_act <- zonkTcType ty_act
-       ; (env1, pp_exp, extra_exp) <- ppr_ty env0 ty_exp
-       ; (env2, pp_act, extra_act) <- ppr_ty env1 ty_act
-       ; return (env2, 
-                  sep [sep [ptext SLIT("Couldn't match expected type") <+> pp_exp, 
-                           nest 7 $
-                              ptext SLIT("against inferred type") <+> pp_act],
-                      nest 2 (extra_exp $$ extra_act)]) }
-
-ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc)
-ppr_ty env ty
-  = do { let (env1, tidy_ty) = tidyOpenType env ty
-       ; (env2, extra) <- ppr_extra env1 tidy_ty
-       ; return (env2, quotes (ppr tidy_ty), extra) }
-
--- (ppr_extra env ty) shows extra info about 'ty'
-ppr_extra :: TidyEnv -> Type -> TcM (TidyEnv, SDoc)
-ppr_extra env (TyVarTy tv)
-  | isSkolemTyVar tv || isSigTyVar tv
-  = return (env1, pprSkolTvBinding tv1)
+        ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
+       }
+
+misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
+misMatchMsg env0 (ty_act, ty_exp)
+  = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
+       (env2, pp_act, extra_act) = ppr_ty env1 ty_act
+        msg = sep [sep [ptext (sLit "Couldn't match expected type") <+> pp_exp, 
+                       nest 7 $
+                              ptext (sLit "against inferred type") <+> pp_act],
+                  nest 2 (extra_exp $$ extra_act)]
+    in
+    (env2, msg)
+
   where
-    (env1, tv1) = tidySkolemTyVar env tv
+    ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
+    ppr_ty env ty
+      = let (env1, tidy_ty) = tidyOpenType env ty
+           (env2, extra)  = ppr_extra env1 tidy_ty
+       in
+       (env2, quotes (ppr tidy_ty), extra)
+
+    -- (ppr_extra env ty) shows extra info about 'ty'
+    ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
+    ppr_extra env (TyVarTy tv)
+      | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
+      = (env1, pprSkolTvBinding tv1)
+      where
+        (env1, tv1) = tidySkolemTyVar env tv
 
-ppr_extra env _ty = return (env, empty)                -- Normal case
+    ppr_extra env _ty = (env, empty)           -- Normal case
 \end{code}