Another checkpointwip/spj-improvement

5 files changed, 197 insertions, 87 deletions

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 176dea284c..040d72914e 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -951,8 +951,8 @@ canEqTyVarTyVar ev eq_rel swapped tv1 tv2
        ; stopWith ev "Equal tyvars" }
 
   | incompat_kind   = incompat
---   | isFmvTyVar tv1  = do_fmv swapped            tv1 xi1 xi2 co1 co2
---   | isFmvTyVar tv2  = do_fmv (flipSwap swapped) tv2 xi2 xi1 co2 co1
+  | isFmvTyVar tv1  = do_fmv swapped            tv1 xi1 xi2 co1 co2
+  | isFmvTyVar tv2  = do_fmv (flipSwap swapped) tv2 xi2 xi1 co2 co1
   | same_kind       = if swap_over then do_swap else no_swap
   | k1_sub_k2       = do_swap   -- Note [Kind orientation for CTyEqCan]
   | otherwise       = no_swap   -- k2_sub_k1
@@ -979,13 +979,20 @@ canEqTyVarTyVar ev eq_rel swapped tv1 tv2
         continueWith (CTyEqCan { cc_ev = new_ev, cc_tyvar = tv1
                                , cc_rhs = xi2, cc_eq_rel = eq_rel })
 
-{-
     -- See Note [Orient equalities with flatten-meta-vars on the left] in TcFlatten
+    -- tv1 is the flatten meta-var
     do_fmv swapped tv1 xi1 xi2 co1 co2
       | same_kind
       = canon_eq swapped tv1 xi1 xi2 co1 co2
-      | otherwise  -- Presumably tv1 `subKind` tv2, which is the wrong way round
-      = ASSERT2( tyVarKind tv1 `isSubKind` typeKind xi2,
+      | otherwise  -- Presumably tv1 :: *, since it is a flatten meta-var,
+                   -- at a kind that has some interesting sub-kind structure.
+                   -- Since the two kinds are not the same, we must have
+                   -- tv1 `subKind` tv2, which is the wrong way round
+                   --   e.g.  (fmv::*) ~ (a::OpenKind)
+                   -- So make a new meta-var and use that:
+                   --         fmv ~ (beta::*)
+                   --         (a::OpenKind) ~ (beta::*)
+      = ASSERT2( k1_sub_k2,
                  ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) $$
                  ppr xi2 <+> dcolon <+> ppr (typeKind xi2) )
         ASSERT2( isWanted ev, ppr ev )  -- Only wanteds have flatten meta-vars
@@ -995,7 +1002,6 @@ canEqTyVarTyVar ev eq_rel swapped tv1 tv2
                                                         tv_ty xi2)
            ; emitWorkNC [new_ev]
            ; canon_eq swapped tv1 xi1 tv_ty co1 (ctEvCoercion new_ev) }
--}
 
     incompat = incompatibleKind ev xi1 k1 xi2 k2
 
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 174f3df769..d5d2b397cb 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -1193,8 +1193,6 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
                              , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs)
                              , text "TcLevel =" <+> ppr tclvl ])
                  ; n_kicked <- kickOutRewritable (ctEvFlavour ev, eq_rel) tv
-                 ; when (isDerived ev) $
-                        (emitDerivedShadows tv)
                  ; addInertEq workItem
                  ; return (Stop ev (ptext (sLit "Kept as inert") <+> ppr_kicked n_kicked)) } }
 
@@ -1267,40 +1265,6 @@ ppr_kicked :: Int -> SDoc
 ppr_kicked 0 = empty
 ppr_kicked n = parens (int n <+> ptext (sLit "kicked out"))
 
-emitDerivedShadows :: TcTyVar -> TcS ()
-emitDerivedShadows new_tv
-  = do { ics <- getInertCans
-       ; mapM_ emit_shadow (get_shadows ics) }
-  where
-    emit_shadow ct = emitNewDerived loc pred
-      where
-        ev = ctEvidence ct
-        pred = ctEvPred ev
-        loc  = ctEvLoc  ev
-
-    get_shadows (IC { inert_eqs      = tv_eqs
-                    , inert_dicts    = dicts
-                    , inert_safehask = safehask
-                    , inert_funeqs   = funeqs
-                    , inert_irreds   = irreds
-                    , inert_model    = model })
-      -- Ignore insolubles
-      = foldDicts get_ct dicts    $
-        foldDicts get_ct safehask $
-        foldFunEqs get_ct funeqs  $
-        foldIrreds get_ct irreds  $
-        foldTyEqs  get_ct tv_eqs []
-      where
-        get_ct ct cts | want_shadow model ct = ct:cts
-                      | otherwise            = cts
-
-    want_shadow model ct
-      =  not (isDerivedCt ct)
-      && not (modelCanRewrite model pred)
-      && (new_tv `elemVarSet` tyVarsOfType pred)
-      where
-         pred = ctPred ct
-
 kickOutAfterUnification :: TcTyVar -> TcS Int
 kickOutAfterUnification new_tv
   = do { ics <- getInertCans
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 25b9b87ce7..2cc42a20e1 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -48,7 +48,7 @@ module TcSMonad (
     emitInsoluble, emitWorkNC, emitWorkCt,
 
     -- The Model
-    InertModel, modelCanRewrite,
+    InertModel,
 
     -- Inert Safe Haskell safe-overlap failures
     addInertSafehask, insertSafeOverlapFailureTcS, updInertSafehask,
@@ -532,6 +532,8 @@ data InertCans
 
        , inert_funeqs :: FunEqMap Ct
               -- All CFunEqCans; index is the whole family head type.
+              -- Hence (by CFunEqCan invariants),
+              -- all Nominal, and all Given/Wanted (no Derived)
 
        , inert_dicts :: DictMap Ct
               -- Dictionaries only, index is the class
@@ -634,36 +636,87 @@ emptyInert
 ---------------
 addInertEq :: Ct -> TcS ()
 -- Precondition: item /is/ canonical
-addInertEq item@(CTyEqCan { cc_ev = ev, cc_eq_rel = eq_rel, cc_tyvar = tv })
-  = do { ics@(IC { inert_count = n
-                 , inert_eqs = old_eqs
-                 , inert_model = old_model }) <- getInertCans
-       ; let new_eqs | isDerived ev = old_eqs
-                     | otherwise    = addTyEq old_eqs tv item
-             new_n = bumpUnsolvedCount ev n
-             new_ics = ics { inert_eqs   = new_eqs
-                           , inert_count = new_n }
-       ; final_ics <- case eq_rel of
-           ReprEq -> return new_ics
-           NomEq | isDerived ev
-                -> return (new_ics { inert_model = extendVarEnv old_model tv item })
-                 | not (modelCanRewrite old_model pred)
-                -> return (new_ics { inert_model = extendVarEnv old_model tv derived_item })
-                 | otherwise
-                 -> do { emitNewDerivedEq loc pred
-                       ; return new_ics }
-       ; setInertCans final_ics }
-  where
-    loc  = ctEvLoc ev
-    pred = ctEvPred ev
-    derived_item = item { cc_ev = CtDerived { ctev_loc = loc, ctev_pred = pred } }
+addInertEq ct
+  = do { traceTcS "addInertEq {" $
+         text "Adding new inert equality:" <+> ppr ct
+       ; ics  <- getInertCans
+       ; ics' <- add_inert_eq ics ct
+       ; setInertCans ics'
+       ; traceTcS "addInertEq }" $ empty }
+
+add_inert_eq :: InertCans -> Ct -> TcS InertCans
+add_inert_eq ics@(IC { inert_count = n
+                     , inert_eqs = old_eqs
+                     , inert_model = old_model })
+             ct@(CTyEqCan { cc_ev = ev, cc_eq_rel = eq_rel, cc_tyvar = tv })
+  | isDerived ev
+  = do { emitDerivedShadows ics tv
+       ; return (ics { inert_model = extendVarEnv old_model tv ct }) }
+
+  | ReprEq <- eq_rel
+  = return (ics { inert_eqs   = addTyEq old_eqs tv ct
+                , inert_count = bumpUnsolvedCount ev n })
+
+  -- Nominal equality, Given/Wanted
+  | modelCanRewrite old_model rw_tvs  -- Shadow of new constraint is
+  = do { emitNewDerivedEq loc pred    -- not inert, so emit it
+       ; return new_ics }
+
+  | otherwise   -- Shadow of new constraint is inert wrt model
+                -- so extend model, and create shadows it can now rewrite
+  = do { emitDerivedShadows ics tv
+       ; return (new_ics { inert_model = new_model }) }
 
-addInertEq item = pprPanic "addInertEq" (ppr item)
+  where
+    loc     = ctEvLoc ev
+    pred    = ctEvPred ev
+    rw_tvs  = tyVarsOfType pred
+    new_ics = ics { inert_eqs   = addTyEq old_eqs tv ct
+                  , inert_count = bumpUnsolvedCount ev n }
+    new_model = extendVarEnv old_model tv derived_ct
+    derived_ct = ct { cc_ev = CtDerived { ctev_loc = loc, ctev_pred = pred } }
+
+add_inert_eq _ ct = pprPanic "addInertEq" (ppr ct)
+
+emitDerivedShadows :: InertCans -> TcTyVar -> TcS ()
+emitDerivedShadows IC { inert_eqs      = tv_eqs
+                      , inert_dicts    = dicts
+                      , inert_safehask = safehask
+                      , inert_funeqs   = funeqs
+                      , inert_irreds   = irreds
+                      , inert_model    = model } new_tv
+  = mapM_ emit_shadow shadows
+  where
+    emit_shadow ct = emitNewDerived loc pred
+      where
+        ev = ctEvidence ct
+        pred = ctEvPred ev
+        loc  = ctEvLoc  ev
+
+    shadows = foldDicts  get_ct dicts    $
+              foldDicts  get_ct safehask $
+              foldFunEqs get_ct funeqs   $
+              foldIrreds get_ct irreds   $
+              foldTyEqs  get_ct tv_eqs []
+      -- Ignore insolubles
+
+    get_ct ct cts | want_shadow ct = ct:cts
+                  | otherwise      = cts
+
+    want_shadow ct
+      =  not (isDerivedCt ct)               -- No need for a shadow of a Derived!
+      && (new_tv `elemVarSet` rw_tvs)       -- New tv can rewrite ct
+      && not (modelCanRewrite model rw_tvs) -- We have not alrady created a shadow
+      where
+        rw_tvs = rewritableTyVars ct
 
-modelCanRewrite :: InertModel -> TcPredType -> Bool
+modelCanRewrite :: InertModel -> TcTyVarSet -> Bool
 -- True if there is any intersection between dom(model) and pred
-modelCanRewrite model pred
-  = foldVarSet ((||) . (`elemVarEnv` model)) False (tyVarsOfType pred)
+modelCanRewrite model tvs = foldVarSet ((||) . (`elemVarEnv` model)) False tvs
+
+rewritableTyVars :: Ct -> TcTyVarSet
+rewritableTyVars (CFunEqCan { cc_tyargs = tys }) = tyVarsOfTypes tys
+rewritableTyVars ct                              = tyVarsOfType (ctPred ct)
 
 --------------
 addInertCan :: Ct -> TcS ()  -- Constraints *other than* equalities
@@ -675,15 +728,15 @@ addInertCan ct
        ; setInertCans (add_item ics ct)
 
        -- Emit shadow derived if necessary
-       ; traceTcS "addInertCan" (vcat [ ppr ct, ppr (isDerived ev), ppr (inert_model ics), ppr (modelCanRewrite (inert_model ics) pred) ])
-       ; when (not (isDerived ev) && modelCanRewrite (inert_model ics) pred)
+       ; when (not (isDerived ev) && modelCanRewrite (inert_model ics) rw_tvs)
               (emitNewDerived (ctEvLoc ev) pred)
 
        ; traceTcS "addInertCan }" $ empty }
 
   where
-    ev   = ctEvidence ct
-    pred = ctEvPred ev
+    rw_tvs = rewritableTyVars ct
+    ev     = ctEvidence ct
+    pred   = ctEvPred ev
 
 add_item :: InertCans -> Ct -> InertCans
 add_item ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys })
diff --git a/testsuite/tests/typecheck/should_compile/T10009.hs b/testsuite/tests/typecheck/should_compile/T10009.hs
index 5b756b2231..ccb89c7402 100644
--- a/testsuite/tests/typecheck/should_compile/T10009.hs
+++ b/testsuite/tests/typecheck/should_compile/T10009.hs
@@ -14,7 +14,7 @@ g _ = f (undefined :: F a)
 
 
 {- ---------------
-[G] UnF (F a) ~ a
+[G] UnF (F b) ~ b
 
 [W] UnF (F beta) ~ beta
 [W] F a ~ F beta
@@ -60,3 +60,93 @@ g _ = f (undefined :: F a)
 
 -- Now we can unify beta!
 -}
+
+
+
+{-
+
+-----
+Inert: [G] fsk_amA ~ b_amr
+       [G] UnF fsk_amy ~ fsk_amA
+       [G} F b_amr ~ fsk_amy
+
+wl: [W] F b_amr ~ F b_amt
+
+work item: [W] UnF (F b_amt) ~ b_amt
+  b_amt is the unification variable
+
+===>      b_amt := s_amF
+
+Inert: [G] fsk_amA ~ b_amr
+       [G] UnF fsk_amy ~ fsk_amA
+       [G} F b_amr ~ fsk_amy
+
+wl: [W] F b_amr ~ F b_amt
+    [W] UnF s_amD ~ s_amF
+
+work item: [W] F b_amt ~ s_amD
+
+
+===>
+wl: [W] F b_amr ~ F b_amt
+    [W] UnF s_amD ~ s_amF
+
+Inert: [G] fsk_amA ~ b_amr
+       [G] UnF fsk_amy ~ fsk_amA
+       [G} F b_amr ~ fsk_amy
+       [W] F s_amF ~ s_amD
+
+===>
+wl: [W] F b_amr ~ F b_amt
+
+Inert: [G] fsk_amA ~ b_amr
+       [G] UnF fsk_amy ~ fsk_amA
+       [G} F b_amr ~ fsk_amy
+       [W] F s_amF ~ s_amD
+       [W] UnF s_amD ~ s_amF
+
+===>
+Inert: [G] fsk_amA ~ b_amr
+       [G] UnF fsk_amy ~ fsk_amA
+       [G} F b_amr ~ fsk_amy
+       [W] UnF s_amD ~ s_amF
+       [W] F s_amF ~ s_amD
+
+wl:
+
+work-item: [W] F b_amr ~ F b_amt
+--> fsk_amy ~ s_amD
+--> s_amD ~ fsk_amy
+
+===>
+Inert: [G] fsk_amA ~ b_amr
+       [G] UnF fsk_amy ~ fsk_amA
+       [G} F b_amr ~ fsk_amy
+       [W] UnF s_amD ~ s_amF
+       [W] F s_amF ~ s_amD
+       [W] s_amD ~ fsk_amy
+
+wl:
+
+work item: [D] UnF s_amD ~ s_amF
+
+--> [D] UnF fsk_amy ~ s_amF
+--> [D] s_amF ~ fsk_amA
+
+===>
+Inert: [G] fsk_amA ~ b_amr
+       [G] UnF fsk_amy ~ fsk_amA
+       [G} F b_amr ~ fsk_amy
+       [W] UnF s_amD ~ s_amF
+       [W] F s_amF ~ s_amD
+       [W] s_amD ~ fsk_amy
+       [D] s_amF ~ fsk_amA
+
+wl:
+
+work item: [D] F s_amF ~ s_amD
+--> F fsk_amA ~ s_amD
+--> s_amd ~ b_amr
+
+
+-}
\ No newline at end of file
diff --git a/testsuite/tests/typecheck/should_fail/IPFail.stderr b/testsuite/tests/typecheck/should_fail/IPFail.stderr
index e9be7add14..963ccd8b54 100644
--- a/testsuite/tests/typecheck/should_fail/IPFail.stderr
+++ b/testsuite/tests/typecheck/should_fail/IPFail.stderr
@@ -1,12 +1,9 @@
-
-IPFail.hs:6:23: error:
-    Couldn't match type ‘Integer’ with ‘Bool’
-    arising from a functional dependency between constraints:
-      ‘?x::Bool’
-        arising from a use of implicit parameter ‘?x’ at IPFail.hs:6:23-24
-      ‘?x::Integer’
-        arising from the implicit-parameter binding for ?x
-        at IPFail.hs:6:9-24
-    In the expression: ?x
-    In the expression: let ?x = 5 in ?x
-    In an equation for ‘f0’: f0 () = let ?x = 5 in ?x
+

+IPFail.hs:6:18: error:

+    Could not deduce (Num Bool) arising from the literal ‘5’

+    from the context: ?x::Int

+      bound by the type signature for: f0 :: (?x::Int) => () -> Bool

+      at IPFail.hs:5:7-31

+    In the expression: 5

+    In the expression: let ?x = 5 in ?x

+    In an equation for ‘f0’: f0 () = let ?x = 5 in ?x