Opened 2 months ago

Closed 4 weeks ago

#15361 closed bug (fixed)

Error message displays redundant equality constraint

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler (Type checker) Version: 8.4.3
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Poor/confusing error message Test Case:
Blocked By: Blocking:
Related Tickets: #14394 Differential Rev(s): Phab:D5002
Wiki Page:

Description

When compiling this program:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

import Data.Kind
import Data.Type.Equality

foo :: forall (a :: Type) (b :: Type) (c :: Type).
       a :~~: b -> a :~~: c
foo HRefl = HRefl

GHC complains thus:

$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:12:13: error:
    • Could not deduce: a ~ c
      from the context: (* ~ *, b ~ a)
        bound by a pattern with constructor:
                   HRefl :: forall k1 (a :: k1). a :~~: a,
                 in an equation for ‘foo’
        at Bug.hs:12:5-9
      ‘a’ is a rigid type variable bound by
        the type signature for:
          foo :: forall a b c. (a :~~: b) -> a :~~: c
        at Bug.hs:(10,1)-(11,27)
      ‘c’ is a rigid type variable bound by
        the type signature for:
          foo :: forall a b c. (a :~~: b) -> a :~~: c
        at Bug.hs:(10,1)-(11,27)
      Expected type: a :~~: c
        Actual type: a :~~: a
    • In the expression: HRefl
      In an equation for ‘foo’: foo HRefl = HRefl
    • Relevant bindings include
        foo :: (a :~~: b) -> a :~~: c (bound at Bug.hs:12:1)
   |
12 | foo HRefl = HRefl
   |             ^^^^^

That * ~ * constraint is entirely redundant.

Change History (13)

comment:1 Changed 2 months ago by goldfire

But you put it there, by matching on heterogeneous equality on types all of kind Type. Do you propose that GHC not mention givens that are implied by other givens?

comment:2 in reply to:  1 Changed 2 months ago by RyanGlScott

Replying to goldfire:

Do you propose that GHC not mention givens that are implied by other givens?

Certainly not, and moreover, GHC already does not mention redundant implied givens in certain situations. In this code:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}

import Data.Type.Equality

data Goo a where
  MkGoo :: (Ord a, a ~ Bool) => a -> Goo a

goo :: Goo a -> a :~: b
goo MkGoo{} = Refl
Bug.hs:10:15: error:
    • Could not deduce: b ~ Bool
      from the context: (Ord a, a ~ Bool)
        bound by a pattern with constructor:
                   MkGoo :: forall a. (Ord a, a ~ Bool) => a -> Goo a,
                 in an equation for ‘goo’
        at Bug.hs:10:5-11
      ‘b’ is a rigid type variable bound by
        the type signature for:
          goo :: forall a b. Goo a -> a :~: b
        at Bug.hs:9:1-23
      Expected type: a :~: b
        Actual type: a :~: a
    • In the expression: Refl
      In an equation for ‘goo’: goo MkGoo {} = Refl
    • Relevant bindings include
        goo :: Goo a -> a :~: b (bound at Bug.hs:10:1)
   |
10 | goo MkGoo{} = Refl
   |               ^^^^

GHC does not bother warning about an Eq a constraint being in the context bound by the MkGoo pattern match, even though it is implied by Ord a.

Moreover, in this code:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}

import Data.Type.Equality

hoo :: Int :~: Int -> a :~: b -> a :~: c
hoo Refl Refl = Refl
Bug.hs:7:17: error:
    • Could not deduce: a ~ c
      from the context: b ~ a
        bound by a pattern with constructor:
                   Refl :: forall k (a :: k). a :~: a,
                 in an equation for ‘hoo’
        at Bug.hs:7:10-13
      ‘a’ is a rigid type variable bound by
        the type signature for:
          hoo :: forall a b c. (Int :~: Int) -> (a :~: b) -> a :~: c
        at Bug.hs:6:1-40
      ‘c’ is a rigid type variable bound by
        the type signature for:
          hoo :: forall a b c. (Int :~: Int) -> (a :~: b) -> a :~: c
        at Bug.hs:6:1-40
      Expected type: a :~: c
        Actual type: a :~: a
    • In the expression: Refl
      In an equation for ‘hoo’: hoo Refl Refl = Refl
    • Relevant bindings include
        hoo :: (Int :~: Int) -> (a :~: b) -> a :~: c (bound at Bug.hs:7:1)
  |
7 | hoo Refl Refl = Refl
  |                 ^^^^

GHC does not warn about an Int ~ Int constraint, even though we "put it there" by matching on a value of type Int :~: Int.

comment:3 Changed 2 months ago by goldfire

I find the second example more convincing than the first. I wonder how we do that...

comment:4 Changed 2 months ago by RyanGlScott

We can fix this issue with the following patch:

  • compiler/typecheck/TcErrors.hs

    diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
    index 95dc152..1098b1f 100644
    a b pp_givens givens 
    18211821    where
    18221822       ppr_given herald (Implic { ic_given = gs, ic_info = skol_info
    18231823                                , ic_env = env })
    1824            = hang (herald <+> pprEvVarTheta gs)
     1824           = hang (herald <+> pprEvVarTheta (mkMinimalBySCs evVarPred gs))
    18251825                2 (sep [ text "bound by" <+> ppr skol_info
    18261826                       , text "at" <+> ppr (tcl_loc env) ])
    18271827

(Where pp_givens is the function that prints out the stuff after from the context:.) Does this sound like a reasonable approach?

comment:5 Changed 2 months ago by goldfire

Well, if it's that easy, yes, I'm quite happy with it. :)

comment:6 Changed 2 months ago by RyanGlScott

Differential Rev(s): Phab:D5002
Status: newpatch

In that case, I'll go for that approach. See Phab:D5002.

comment:7 Changed 8 weeks ago by simonpj

I was puzzled about why redundant givens are sometimes reported and sometimes not. Here's the deal

  • For each implication GHC figures out, during constraint solving, whether the implication binds any equalities. This is used to guide equality float-out, and is recorded in the implication in the ic_no_eqs field.
  • The "whether binds any equalities" test is performed on the canonicalised, inert givens, in TcSMonad.getNoGivenEqs. See Note [When does an implication have given equalities?].
  • If an implication binds * ~ * only (call it situation (A)), we'll discard that Given, and mark the implication as ic_no_eqs = True.
  • But if an implication binds * ~ * and a ~ b, situation (B), the ic_no_eqs field will be set False.
  • When reporting an equality error, we report givens only from implications with ic_no_eqs = False. That makes sense. But it'll discard situation (A), and keep situation (B).
  • For the implications we keep, we report all original, user-written givens. Hence the reported * ~ *.

So that explain the behavior you see. For example for hoo in comment:2, the Int :~: Int binds no equalities because when Int ~ Int is solved we get nothing. So it is not reported.

I suppose, therefore, that the solution you suggest is no unreasonable, provided you write Note to explain. In particular

  • mkMinimalBySCs happens to eliminate reflexive equalities, as well as superclasses. (Why? See Note [Remove redundant provided dicts] in TcPatSyn`.
  • Explain how a given * ~ * can arise.

comment:8 in reply to:  7 Changed 8 weeks ago by RyanGlScott

Replying to simonpj:

I suppose, therefore, that the solution you suggest is no unreasonable, provided you write Note to explain.

Sure thing. I've updated Phab:D5002.

comment:9 Changed 6 weeks ago by bgamari

Milestone: 8.6.18.8.1

These won't be fixed for in GHC 8.6.

comment:10 Changed 6 weeks ago by Krzysztof Gogolewski <krz.gogolewski@…>

In c552feea/ghc:

Suppress redundant givens during error reporting

Summary:
When GHC reports that it cannot solve a constraint in error
messages, it often reports what given constraints it has in scope.
Unfortunately, sometimes redundant constraints (like `* ~ *`, from
#15361) can sneak in. The fix is simple: blast away these redundant
constraints using `mkMinimalBySCs`.

Test Plan: make test TEST=T15361

Reviewers: simonpj, bgamari

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #15361

Differential Revision: https://phabricator.haskell.org/D5002

comment:11 Changed 6 weeks ago by monoidal

Status: patchmerge

comment:12 Changed 4 weeks ago by RyanGlScott

Milestone: 8.8.18.6.1

This was marked as merge, but not milestoned properly.

comment:13 Changed 4 weeks ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.