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 non-injective 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 non-injective 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 RyanGlScott

This started happening after commit a920404fb12fb52a59e4f728cce4d662a418c5f8 (Fix TcSimplify.decideQuantification for kind variables).

comment:2 Changed 12 months ago by RyanGlScott

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 = 
    147147  UDFM (M.insert (getKey $ getUnique k) (TaggedVal v i) m) (i + 1)
    148148
    149149addToUDFM_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)
     150addToUDFM_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
    152157
    153158addToUDFM_Directly_C
    154159  :: (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 simonpj

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 goldfire

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 top-level 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 simonpj

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 flat-skols] 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 goldfire

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 simonpj

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 sub-problems 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 goldfire

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 simonpj

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.

Last edited 12 months ago by simonpj (previous) (diff)

comment:10 Changed 12 months ago by RyanGlScott

Milestone: 8.6.18.8.1

comment:11 Changed 9 months ago by osa1

Milestone: 8.8.18.10.1

Bumping milestones of low-priority tickets.

comment:12 Changed 8 months ago by pacak

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
  |     ^^^^^^^^^^^^^^^^^^^^
Note: See TracTickets for help on using tickets.