Opened 12 days ago

Last modified 9 days ago

#15361 new bug

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):
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 (5)

comment:1 Changed 12 days 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 12 days 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 12 days ago by goldfire

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

comment:4 Changed 9 days 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 9 days ago by goldfire

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

Note: See TracTickets for help on using tickets.