Type families: bug fixes

diff --git a/compiler/basicTypes/Var.lhs b/compiler/basicTypes/Var.lhs
index cb0a11b..eec6c80 100644 (file)
--- a/compiler/basicTypes/Var.lhs
+++ b/compiler/basicTypes/Var.lhs
@@ -273,8 +273,7 @@ mkTyVar name kind = ASSERT( not (isCoercionKind kind ) )
 
 mkTcTyVar :: Name -> Kind -> TcTyVarDetails -> TyVar
 mkTcTyVar name kind details
-  = -- TOM: no longer valid assertion? 
-    -- ASSERT( not (isCoercionKind kind) )
+  = -- NB: 'kind' may be a coercion kind; cf, 'TcMType.newMetaCoVar'
     TcTyVar {  varName    = name,
                realUnique = getKeyFastInt (nameUnique name),
                varType  = kind,
@@ -391,8 +390,9 @@ isLocalIdVar (LocalId {}) = True
 isLocalIdVar _            = False
 
 isCoVar :: Var -> Bool
-isCoVar (v@(TyVar {})) = isCoercionVar v
-isCoVar _              = False
+isCoVar (v@(TyVar {}))             = isCoercionVar v
+isCoVar (TcTyVar {varType = kind}) = isCoercionKind kind  -- used during solving
+isCoVar _                          = False
 
 -- | 'isLocalVar' returns @True@ for type variables as well as local 'Id's
 -- These are the variables that we need to pay attention to when finding free

diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs
index 1a8efe2..c009ebe 100644 (file)
--- a/compiler/typecheck/Inst.lhs
+++ b/compiler/typecheck/Inst.lhs
@@ -45,7 +45,8 @@ module Inst (
         mkIdEqInstCo, mkSymEqInstCo, mkLeftTransEqInstCo,
         mkRightTransEqInstCo, mkAppEqInstCo,
         isValidWantedEqInst,
-       eitherEqInst, mkEqInst, mkEqInsts, mkWantedEqInst, finalizeEqInst, 
+       eitherEqInst, mkEqInst, mkEqInsts, mkWantedEqInst,
+        wantedToLocalEqInst, finalizeEqInst, 
        eqInstType, updateEqInstCoercion,
        eqInstCoercion, eqInstTys
     ) where
@@ -1095,6 +1096,15 @@ mkWantedEqInst pred@(EqPred ty1 ty2)
        }
 mkWantedEqInst pred = pprPanic "mkWantedEqInst" (ppr pred)
 
+-- Turn a wanted equality into a local that propagates the uninstantiated
+-- coercion variable as witness.  We need this to propagate wanted irreds into
+-- attempts to solve implication constraints.
+--
+wantedToLocalEqInst :: Inst -> Inst
+wantedToLocalEqInst eq@(EqInst {tci_co = Left cotv})
+  = eq {tci_co = Right (mkTyVarTy cotv)}
+wantedToLocalEqInst eq = eq
+
 -- Turn a wanted into a local EqInst (needed during type inference for
 -- signatures) 
 --

diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 8a5ad1a..c285c5e 100644 (file)
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -1673,7 +1673,7 @@ data RedEnv
           , red_try_me :: Inst -> WhatToDo
           , red_improve :: Bool                -- True <=> do improvement
           , red_givens :: [Inst]               -- All guaranteed rigid
-                                               -- Always dicts
+                                               -- Always dicts & equalities
                                                -- but see Note [Rigidity]
           , red_stack  :: (Int, [Inst])        -- Recursion stack (for err msg)
                                                -- See Note [RedStack]
@@ -1806,8 +1806,12 @@ reduceContext env wanteds0
          -- as "given"   all the dicts that were originally given, 
          --              *or* for which we now have bindings, 
          --              *or* which are now irreds
-       ; let implic_env = env { red_givens = givens ++ bound_dicts ++
-                                              dict_irreds }
+          -- NB: Equality irreds need to be converted, as the recursive 
+          --     invocation of the solver will still treat them as wanteds
+          --     otherwise.
+       ; let implic_env = env { red_givens 
+                                   = givens ++ bound_dicts ++
+                                     map wantedToLocalEqInst dict_irreds }
        ; (implic_binds_s, implic_irreds_s) 
             <- mapAndUnzipM (reduceImplication implic_env) wanted_implics
        ; let implic_binds  = unionManyBags implic_binds_s
@@ -1928,6 +1932,12 @@ reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state
     -- Base case: we're done!
 reduce :: RedEnv -> Inst -> Avails -> TcM Avails
 reduce env wanted avails
+
+    -- We don't reduce equalities here (and they must not end up as irreds
+    -- in the Avails!)
+  | isEqInst wanted
+  = return avails
+
     -- It's the same as an existing inst, or a superclass thereof
   | Just _ <- findAvail avails wanted
   = do { traceTc (text "reduce: found " <+> ppr wanted)
@@ -2388,6 +2398,9 @@ extractResults (Avails _ avails) wanteds
       = return (binds, bound_dicts, irreds)
 
     go binds bound_dicts irreds done (w:ws)
+      | isEqInst w
+      = go binds bound_dicts (w:irreds) done' ws
+
       | Just done_ids@(done_id : rest_done_ids) <- lookupFM done w
       = if w_id `elem` done_ids then
           go binds bound_dicts irreds done ws

diff --git a/compiler/typecheck/TcTyFuns.lhs b/compiler/typecheck/TcTyFuns.lhs
index 2ad6233..84453bc 100644 (file)
--- a/compiler/typecheck/TcTyFuns.lhs
+++ b/compiler/typecheck/TcTyFuns.lhs
@@ -442,17 +442,21 @@ deriveEqInst rewrite ty1 ty2 co
 
 instance Outputable RewriteInst where
   ppr (RewriteFam {rwi_fam = fam, rwi_args = args, rwi_right = rhs, rwi_co =co})
-    = hsep [ ppr co <+> text "::" 
+    = hsep [ pprEqInstCo co <+> text "::" 
            , ppr (mkTyConApp fam args)
            , text "~>"
            , ppr rhs
            ]
   ppr (RewriteVar {rwi_var = tv, rwi_right = rhs, rwi_co =co})
-    = hsep [ ppr co <+> text "::" 
+    = hsep [ pprEqInstCo co <+> text "::" 
            , ppr tv
            , text "~>"
            , ppr rhs
            ]
+
+pprEqInstCo :: EqInstCo -> SDoc
+pprEqInstCo (Left cotv) = ptext (sLit "Wanted") <+> ppr cotv
+pprEqInstCo (Right co)  = ptext (sLit "Local") <+> ppr co
 \end{code}
 
 The following functions turn an arbitrary equality into a set of normal
@@ -579,7 +583,13 @@ checkOrientation :: Type -> Type -> EqInstCo -> Inst -> TcM [RewriteInst]
 -- NB: We cannot assume that the two types already have outermost type
 --     synonyms expanded due to the recursion in the case of type applications.
 checkOrientation ty1 ty2 co inst
-  = go ty1 ty2
+  = do { traceTc $ ptext (sLit "checkOrientation of ") <+> 
+                   pprEqInstCo co <+> text "::" <+> 
+                   ppr ty1 <+> text "~" <+> ppr ty2
+       ; eqs <- go ty1 ty2
+       ; traceTc $ ptext (sLit "checkOrientation returns") <+> ppr eqs
+       ; return eqs
+       }
   where
       -- look through synonyms
     go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
@@ -1050,8 +1060,7 @@ substitute eqs locals wanteds = subst eqs [] emptyBag locals wanteds
       = return (res, binds, locals, wanteds)
     subst (eq@(RewriteVar {rwi_var = tv, rwi_right = ty, rwi_co = co}):eqs) 
           res binds locals wanteds
-      = do { traceTc $ ptext (sLit "TcTyFuns.substitute:") <+> ppr tv <+>
-                       ptext (sLit "->") <+> ppr ty
+      = do { traceTc $ ptext (sLit "TcTyFuns.substitute:") <+> ppr eq
            ; let coSubst = zipOpenTvSubst [tv] [eqInstCoType co]
                  tySubst = zipOpenTvSubst [tv] [ty]
            ; eqs'               <- mapM (substEq eq coSubst tySubst) eqs