[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       |           Version:  8.4.3
  (Type checker)                     |
           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:
-------------------------------------+-------------------------------------
 When compiling this program:

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

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