Re: [GHC] #15361: Error message displays redundant equality constraint

11 Jul 2018

      #15361: Error message displays redundant equality constraint
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.4.3
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Poor/confusing    |  Unknown/Multiple
  error message                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #14394            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Replying to [comment:1 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:

 {{{#!hs
 {-# 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:

 {{{#!hs
 {-# 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`.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15361#comment:2
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler