Fix ASSERT failure in TcErrors
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 29 Mar 2017 13:57:21 +0000 (14:57 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Wed, 29 Mar 2017 13:57:21 +0000 (14:57 +0100)
This fixes Trac #13494, by improving

   commit e0ad55f894a8d85dcc099c33c63cfe3d4515d464
   Author: Simon Peyton Jones <simonpj@microsoft.com>
   Date:   Mon Mar 27 10:32:08 2017 +0100

   Fix error-message suppress on given equalities

which in turn was a fix to #13446

compiler/typecheck/TcErrors.hs
testsuite/tests/indexed-types/should_fail/T2627b.stderr
testsuite/tests/indexed-types/should_fail/T6123.stderr
testsuite/tests/indexed-types/should_fail/T7354.stderr

index 84a28a7..9701637 100644 (file)
@@ -1474,22 +1474,21 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
         , report
         ]
 
-  -- So tv is a meta tyvar (or started that way before we
-  -- generalised it).  So presumably it is an *untouchable*
-  -- meta tyvar or a SigTv, else it'd have been unified
   | OC_Occurs <- occ_check_expand
-  , insoluble_occurs_check
-         -- See Note [Occurs check error] in TcCanonical
-  = do { let occCheckMsg = important $ addArising (ctOrigin ct) $
-                           hang (text "Occurs check: cannot construct the infinite" <+> what <> colon)
+    -- We report an "occurs check" even for  a ~ F t a, where F is a type
+    -- function; it's not insouble (because in principle F could reduce)
+    -- but we have certainly been unable to solve it
+    -- See Note [Occurs check error] in TcCanonical
+  = do { let main_msg = addArising (ctOrigin ct) $
+                        hang (text "Occurs check: cannot construct the infinite" <+> what <> colon)
                               2 (sep [ppr ty1, char '~', ppr ty2])
+
              extra2 = important $ mkEqInfoMsg ct ty1 ty2
 
-             interesting_tyvars
-               = filter (not . noFreeVarsOfType . tyVarKind) $
-                 filter isTyVar $
-                 fvVarList $
-                 tyCoFVsOfType ty1 `unionFV` tyCoFVsOfType ty2
+             interesting_tyvars = filter (not . noFreeVarsOfType . tyVarKind) $
+                                  filter isTyVar $
+                                  fvVarList $
+                                  tyCoFVsOfType ty1 `unionFV` tyCoFVsOfType ty2
              extra3 = relevant_bindings $
                       ppWhen (not (null interesting_tyvars)) $
                       hang (text "Type variable kinds:") 2 $
@@ -1497,7 +1496,8 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
                                 interesting_tyvars)
 
              tyvar_binding tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
-       ; mkErrorMsgFromCt ctxt ct $ mconcat [occCheckMsg, extra2, extra3, report] }
+       ; mkErrorMsgFromCt ctxt ct $
+         mconcat [important main_msg, extra2, extra3, report] }
 
   | OC_Bad <- occ_check_expand
   = do { let msg = vcat [ text "Cannot instantiate unification variable"
@@ -1546,6 +1546,9 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
        ; mkErrorMsgFromCt ctxt ct (mconcat [msg, tv_extra, report]) }
 
   -- Nastiest case: attempt to unify an untouchable variable
+  -- So tv is a meta tyvar (or started that way before we
+  -- generalised it).  So presumably it is an *untouchable*
+  -- meta tyvar or a SigTv, else it'd have been unified
   -- See Note [Error messages for untouchables]
   | (implic:_) <- cec_encl ctxt   -- Get the innermost context
   , Implic { ic_env = env, ic_given = given
index 1a09bd8..63f11b9 100644 (file)
@@ -1,13 +1,9 @@
 
 T2627b.hs:20:24: error:
-    • Couldn't match type ‘b0’ with ‘Dual (Dual b0)’
+    • Occurs check: cannot construct the infinite type:
+        b0 ~ Dual (Dual b0)
         arising from a use of ‘conn’
-        ‘b0’ is untouchable
-          inside the constraints: b ~ W e f
-          bound by a pattern with constructor:
-                     Wr :: forall e f. e -> Comm f -> Comm (W e f),
-                   in an equation for ‘conn’
-          at T2627b.hs:20:14-19
+      The type variable ‘b0’ is ambiguous
     • In the expression: conn undefined undefined
       In an equation for ‘conn’:
           conn (Rd k) (Wr a r) = conn undefined undefined
index eafd27c..0ae1a5e 100644 (file)
@@ -1,6 +1,7 @@
 
 T6123.hs:10:14: error:
-    • Couldn't match type ‘a0’ with ‘Id a0’ arising from a use of ‘cid’
+    • Occurs check: cannot construct the infinite type: a0 ~ Id a0
+        arising from a use of ‘cid’
       The type variable ‘a0’ is ambiguous
     • In the expression: cid undefined
       In an equation for ‘cundefined’: cundefined = cid undefined
index f4c3c0d..b7b70b8 100644 (file)
@@ -1,8 +1,7 @@
 
 T7354.hs:28:11: error:
-    • Couldn't match type ‘p’ with ‘Base t (Prim [p] p)’
-      ‘p’ is a rigid type variable bound by
-        the inferred type of foo :: Prim [p] p -> t at T7354.hs:28:1-13
+    • Occurs check: cannot construct the infinite type:
+        p ~ Base t (Prim [p] p)
       Expected type: Prim [p] p -> Base t (Prim [p] p)
         Actual type: Prim [p] p -> p
     • In the first argument of ‘ana’, namely ‘alg’