Opened 3 years ago

Closed 6 months ago

#5763 closed bug (fixed)

Confusing error message

Reported by: simonpj Owned by: simonpj
Priority: normal Milestone: 7.10.1
Component: Compiler Version: 7.2.2
Keywords: Cc: dimitris@…, hackage.haskell.org@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description

For test indexed-types/should_fail/T4272 we get this type error

T4272.hs:11:16:
    Occurs check: cannot construct the infinite type:
      x0 = TermFamily x0 x0
    Expected type: TermFamily x0 x0
      Actual type: TermFamily a a
    In the first argument of `prune', namely `t'
    In the expression: prune t (terms (undefined :: TermFamily a a))
    In an equation for `laws':
        laws t = prune t (terms (undefined :: TermFamily a a))

It's not at all obvious why unifying (TermFamily x0 x0) with (TermFamily a a) should yield an occurs check. Especially as TermFamily is a type function with arity 1, and x0 is a unification variable. So the natural way to solve this constraint would be to unify x0 with a, and then the constraint is satisfied.

What goes wrong is that there is another insolube constraint (which is also reported):

T4272.hs:11:19:
    Could not deduce (a ~ TermFamily x0 x0)
    from the context (TermLike a)
      bound by the type signature for
                 laws :: TermLike a => TermFamily a a -> b
      at T4272.hs:11:1-54
      `a' is a rigid type variable bound by
          the type signature for laws :: TermLike a => TermFamily a a -> b
          at T4272.hs:11:1
    In the return type of a call of `terms'
    In the second argument of `prune', namely
      `(terms (undefined :: TermFamily a a))'
    In the expression: prune t (terms (undefined :: TermFamily a a))

The constraint solver finds this latter constraint, can't solve it, but still uses it to simplify the first one, by substituting (TermFamily x0 x0) for a; and that is what gives the occurs check error.

I don't think that we should use insoluble constraints to rewrite unsolved constraints. But it's delicate, so I am not trying to fiddle right now. Hence making this ticket.

(Incidentally, it's not a regression; it's been like this forever.)

Change History (10)

comment:1 Changed 3 years ago by simonpj

  • Priority changed from normal to high

I'll make it high priority to make sure I look at it for 7.6. But it's not really that serious.

comment:2 Changed 3 years ago by simonpj

  • Test Case changed from indexed-types/should_fail/T4272 to indexed-types/should_fail/T5763

comment:3 Changed 3 years ago by simonpj

  • Owner set to simonpj

comment:4 Changed 3 years ago by igloo

  • Milestone changed from 7.6.1 to 7.6.2

comment:5 Changed 2 years ago by liyang

  • Cc hackage.haskell.org@… added

comment:6 Changed 23 months ago by wira

can i know too problem solving

comment:7 Changed 11 months ago by thoughtpolice

  • Priority changed from high to normal

Lowering priority (these tickets are assigned to older versions, so they're getting bumped as they've been around for a while).

comment:8 Changed 11 months ago by thoughtpolice

  • Milestone changed from 7.6.2 to 7.10.1

Moving to 7.10.1.

comment:9 Changed 6 months ago by thomie

Is this problem solved?

T4272 doesn't show the Occurs check message anymore (as also noted by SPJ in da71a9524ffff0865222127bef09fd04a1359a53), but maybe this is incidental? I can not find test T5763 anywhere, so I'll leave this open for now.

Output of running the command "git show 0b3c3c81792c88ee40687f86bed4935e721dabe0 testsuite/tests/indexed-types/should_fail/T4272.stderr":

Author: Dimitrios.Vytiniotis <>
Date:   Wed Apr 4 14:41:11 2012 +0100

    Error message modifications following ghc-new-solver modifications

diff --git a/testsuite/tests/indexed-types/should_fail/T4272.stderr b/testsuite/tests/indexed-types/should_fail/T4272.stderr
index 24f0cbd..e809d9c 100644
--- a/testsuite/tests/indexed-types/should_fail/T4272.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4272.stderr
@@ -1,29 +1,6 @@
 
-T4272.hs:11:16:
-    Couldn't match type `TermFamily (TermFamily x0 x0)'
-                  with `TermFamily x0'
-    NB: `TermFamily' is a type function, and may not be injective
-    The type variable `x0' is ambiguous
-    Possible fix: add a type signature that fixes these type variable(s)
-    Expected type: TermFamily x0 x0
-      Actual type: TermFamily a a
-    In the first argument of `prune', namely `t'
-    In the expression: prune t (terms (undefined :: TermFamily a a))
-    In an equation for `laws':
-        laws t = prune t (terms (undefined :: TermFamily a a))
-
-T4272.hs:11:16:
-    Occurs check: cannot construct the infinite type:
-      x0 = TermFamily x0 x0
-    Expected type: TermFamily x0 x0
-      Actual type: TermFamily a a
-    In the first argument of `prune', namely `t'
-    In the expression: prune t (terms (undefined :: TermFamily a a))
-    In an equation for `laws':
-        laws t = prune t (terms (undefined :: TermFamily a a))
-
-T4272.hs:11:19:
-    Could not deduce (a ~ TermFamily x0 x0)
+T4272.hs:11:26:
+    Could not deduce (a ~ TermFamily a a)
     from the context (TermLike a)
       bound by the type signature for
                  laws :: TermLike a => TermFamily a a -> b
@@ -31,7 +8,10 @@ T4272.hs:11:19:
       `a' is a rigid type variable bound by
           the type signature for laws :: TermLike a => TermFamily a a -> b
           at T4272.hs:10:16
-    In the return type of a call of `terms'
+    Expected type: TermFamily a (TermFamily a a)
+      Actual type: TermFamily a a
+    In the first argument of `terms', namely
+      `(undefined :: TermFamily a a)'
     In the second argument of `prune', namely
       `(terms (undefined :: TermFamily a a))'
     In the expression: prune t (terms (undefined :: TermFamily a a))

comment:10 Changed 6 months ago by simonpj

  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case indexed-types/should_fail/T5763 deleted

Well we indeed no longer use insoluble constraints to rewrite others, so yes, I think we can close this.

Simon

Note: See TracTickets for help on using tickets.