Opened 12 months ago
Last modified 8 months ago
#15621 new bug
Error message involving type families points to wrong location
Reported by:  RyanGlScott  Owned by:  

Priority:  normal  Milestone:  8.10.1 
Component:  Compiler (Type checker)  Version:  8.4.3 
Keywords:  TypeFamilies  Cc:  
Operating System:  Unknown/Multiple  Architecture:  Unknown/Multiple 
Type of failure:  Poor/confusing error message  Test Case:  
Blocked By:  Blocking:  
Related Tickets:  Differential Rev(s):  
Wiki Page: 
Description
Consider the following program:
{# LANGUAGE TypeFamilies #} {# LANGUAGE TypeOperators #} module Bug where import Data.Type.Equality type family F a f :: () f = let a :: F Int :~: F Int a = Refl b :: F Int :~: F Bool b = Refl in ()
This doesn't typecheck, which isn't surprising, since F Int
doesn't equal F Bool
in the definition of b
. What is surprising is where the error message points to:
$ /opt/ghc/8.4.3/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:12:11: error: • Couldn't match type ‘F Int’ with ‘F Bool’ Expected type: F Int :~: F Int Actual type: F Bool :~: F Bool NB: ‘F’ is a noninjective type family • In the expression: Refl In an equation for ‘a’: a = Refl In the expression: let a :: F Int :~: F Int a = Refl b :: F Int :~: F Bool .... in ()  12  a = Refl  ^^^^
This claims that the error message arises from the definition of a
, which is completely wrong! As evidence, if you comment out b
, then the program typechecks again.
Another interesting facet of this bug is that if you comment out a
:
{# LANGUAGE TypeFamilies #} {# LANGUAGE TypeOperators #} module Bug where import Data.Type.Equality type family F a f :: () f = let { a :: F Int :~: F Int a = Refl } b :: F Int :~: F Bool b = Refl in ()
Then the error message will actually point to b
this time:
$ /opt/ghc/8.4.3/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:15:11: error: • Couldn't match type ‘F Int’ with ‘F Bool’ Expected type: F Int :~: F Bool Actual type: F Bool :~: F Bool NB: ‘F’ is a noninjective type family • In the expression: Refl In an equation for ‘b’: b = Refl In the expression: let b :: F Int :~: F Bool b = Refl in ()  15  b = Refl  ^^^^
The use of type families appears to be important to triggering this bug, since I can't observe this behavior without the use of F
.
This is a regression that was introduced at some point between GHC 8.0.2 and 8.2.2, since 8.2.2 gives the incorrect error message shown above, while 8.0.2 points to the right location:
$ /opt/ghc/8.0.2/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:15:11: error: • Couldn't match type ‘F Int’ with ‘F Bool’ Expected type: F Int :~: F Bool Actual type: F Int :~: F Int NB: ‘F’ is a type function, and may not be injective • In the expression: Refl In an equation for ‘b’: b = Refl In the expression: let a :: F Int :~: F Int a = Refl b :: F Int :~: F Bool .... in ()
Change History (12)
comment:1 Changed 12 months ago by
comment:2 Changed 12 months ago by
In particular, applying this change on top of the previous commit (d4fa088350913233520ffa7163ef188a63666262) is enough to make the bug surface:

compiler/utils/UniqDFM.hs
diff git a/compiler/utils/UniqDFM.hs b/compiler/utils/UniqDFM.hs index 10e8aa9..3d4b1d6 100644
a b addToUDFM (UDFM m i) k v = 147 147 UDFM (M.insert (getKey $ getUnique k) (TaggedVal v i) m) (i + 1) 148 148 149 149 addToUDFM_Directly :: UniqDFM elt > Unique > elt > UniqDFM elt 150 addToUDFM_Directly (UDFM m i) u v = 151 UDFM (M.insert (getKey u) (TaggedVal v i) m) (i + 1) 150 addToUDFM_Directly (UDFM m i) u v 151 = UDFM (M.insertWith tf (getKey u) (TaggedVal v i) m) (i + 1) 152 where 153 tf (TaggedVal new_v _) (TaggedVal _ old_i) = TaggedVal new_v old_i 154  Keep the old tag, but insert the new value 155  This means that udfmToList typically returns elements 156  in the order of insertion, rather than the reverse 152 157 153 158 addToUDFM_Directly_C 154 159 :: (elt > elt > elt) > UniqDFM elt > Unique > elt > UniqDFM elt
Since that comment mentions that udfmToList
now returns elements in a different order than it did previously, I wonder if there is some code which was sensitive to udfmToList
's order that wasn't updated properly...
comment:3 Changed 12 months ago by
We have Refl :: forall a. Refl a a
So from the defn of a
we instantiate Refl
with a := alpha
, and get
[W] c1 :: alpha ~ F Int  Line 12 [W] c2 :: alpha ~ F Int  Line 12
Each constraint carries its birth location, which I show here.
Same for b
, instantiating Refl
with a := beta
:
[W] c3 :: beta ~ F Int  Line 15 [W] c4 :: beta ~ F Bool  Line 15
Then depending on the order in which we try to solve, we might do
alpha := beta beta := F Bool  solves c4
Now, substituting for these unified varaiables, we get
[W] c1 :: F Bool ~ F Int  Line 12 [W] c2 :: F Bool ~ F Int  Line 12 [W] C3 :: F Bool ~ F Int  Line 15
Since these are identical, we pick one; and alas, it is c1
.
So that's why we get a bogus message.
Richard, I'd be interested in your views.
comment:4 Changed 12 months ago by
This sniffs awfully like wanteds rewriting wanteds.
I don't agree with the details in comment:3. You have constraints like alpha ~ F Int
. But CTyEqCan
documents "rhs ... has no toplevel function". So these constraints look malformed. I would expect an intervening flatten metavar, which may change what's going on here.
comment:5 Changed 12 months ago by
I don't agree with the details in comment:3.
Yes, I was abbreviating! What we get is
 From 'a' [W] fsk1 ~ alpha (CTyEqCan) [W] F Int ~ fsk1 (CFunEqCan) [W] fsk1 ~ alpha (CTyEqCan)  From 'b' [W] fsk1 ~ beta (CTyEqCan) [W] fsk2 ~ beta (CTyEqCan) [W] F Bool ~ fsk2 (CFunEqCan)
Then from [W] fsk1 ~ alpha
and [W] fsk1 ~ beta
we get [D] alpha ~ beta
.
And that leads to alpha := beta
. The beta := F Bool
comes during unflattening.
The purpose of the Derived constraints is precisely to lead to unifications, exactly as we do here. So we probalbly don't want to stop that happening.
Why do we get fsk1 ~ alpha
rather than alpha ~ fsk1
followed by unification?
See Note [Canonical orientation for tyvar/tyvar equality constraints]
in
TcCanonical
, and Note [Eliminate flatskols]
in TcType
.
I think this ticket is closely related to Trac #14185. If we put the constraints
from the two definitions into separate implication constraints (with no skolems
and no givens), I think the Right Thing would happen. You'll see some half
written code, commented out, around alwaysBuildImplication
in TcUnify
.
I think that'd fix this.
But I didn't have time to review all the error message wibbles  probably many are improvements. Does anyone else want to have a go? The code is there!
comment:6 Changed 12 months ago by
I agree that the fix for #14185 will fix this precise example, but will it fix all such examples? What if there is a Refl :: F Int :~: F Int
and a Refl :: F Int :~: F Bool
in the same function? Then we'd be right back here. So I think #14185 is a bit of a red herring here. (I also think that fix might not fix all cases of #14185 itself.)
With the way deriveds currently work, the "wanteds don't rewrite wanteds" story applies really only to skolems (which can't be "improved" through deriveds). Here, we want it also to apply to unification variables. Yet we also want to keep the work that deriveds do in other cases. I'm out of time now, but I don't think this will be so easy, somehow...
comment:7 Changed 12 months ago by
What if there is a Refl :: F Int :~: F Int and a Refl :: F Int :~: F Bool in the same function?
It's fine. Each type signature will give rise to its own implication constraint (indeed already does, except that it is optimised away for signatures that are monotypes).
So I think that #14185 is not a red herring at all!
I agree that there is a tension here. The whole point of Deriveds, the only reason they exist, is so that we can more vigorously rewrite wanteds with wanteds, and thus find equalities that must hold in any ultimate solution. The trouble is that there may still be a choice of which unifications to do in which order, and that affects error messages. I'm proposing our implication constraints as a way to keep the two subproblems separate.
(They won't stay separate, because we'll float out any unsolved equality constraints  and indeed deliberately so, so that they can meet friends from other equality constraints and we can learn more equalities thereby. But they will at least begin separate.
comment:8 Changed 12 months ago by
But what about a function that mentions
let x = (Refl :: F Int :~: F Int) `seq` (Refl :: F Int :~: F Bool) `seq` ()
We'll get the error on the wrong line, won't we? The solution to #14185 improves the status quo, but only by a lucky coincidence (that the problems in both tickets stem from two different functions). What's nice about #14185 is that it prevents the error from jumping arbitrarily far in a file, but I still don't think it's the real solution to the problem.
comment:9 Changed 12 months ago by
The solution to #14185 improves the status quo, but only by a lucky coincidence (that the problems in both tickets stem from two different functions)
NO, as I say in comment:7, each type signature (in a binding, or in an expression) makes a new implication constraint, so that'll keep their constraints separate.
comment:10 Changed 12 months ago by
Milestone:  8.6.1 → 8.8.1 

comment:11 Changed 9 months ago by
Milestone:  8.8.1 → 8.10.1 

Bumping milestones of lowpriority tickets.
comment:12 Changed 8 months ago by
One more example, figuring out why ghc complains on an innocent looking line took a bit of time.
% cat foo.hs
module P (o_O) where import GHC.Types o_O :: Maybe Any o_O = do present < pure True if present then undefined :: Maybe Int else undefined :: Maybe Int
% ghc O foo.hs [1 of 1] Compiling P ( foo.hs, foo.o ) foo.hs:7:5: error: • Couldn't match type ‘Any’ with ‘Int’ Expected type: Maybe Any Actual type: Maybe Int • In a stmt of a 'do' block: present < pure True In the expression: do present < pure True if present then undefined :: Maybe Int else undefined :: Maybe Int In an equation for ‘o_O’: o_O = do present < pure True if present then undefined :: Maybe Int else undefined :: Maybe Int  7  present < pure True  ^^^^^^^^^^^^^^^^^^^^
This started happening after commit a920404fb12fb52a59e4f728cce4d662a418c5f8 (
Fix TcSimplify.decideQuantification for kind variables
).