[GHC] #10614: Show constraints in ``Found hole...''

8 Jul 2015

      #10614: Show constraints in ``Found hole...''
-------------------------------------+-------------------------------------
              Reporter:  bjmprice    |             Owner:
                  Type:  feature     |            Status:  new
  request                            |         Milestone:
              Priority:  normal      |           Version:  7.10.1
             Component:  Compiler    |  Operating System:  Unknown/Multiple
              Keywords:              |   Type of failure:  None/Unknown
          Architecture:              |        Blocked By:
  Unknown/Multiple                   |   Related Tickets:
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
 Currently it is not clear when types are known equal. Consider writing
 castWith:
 {{{#!hs
 {-# LANGUAGE GADTs , TypeOperators #-}
 import Data.Type.Equality hiding (castWith)

 castWith :: a :~: b -> a -> b
 castWith Refl x = _
 }}}

 which results in

 {{{
 TypeEq.hs:5:19: error:
     Found hole: _ :: b
     Where: ‘b’ is a rigid type variable bound by
                the type signature for: castWith :: a :~: b -> a -> b
                at TypeEq.hs:4:13
     Relevant bindings include
       x :: a (bound at TypeEq.hs:5:15)
       castWith :: a :~: b -> a -> b (bound at TypeEq.hs:5:1)
     In the expression: _
     In an equation for ‘castWith’: castWith Refl x = _
 }}}

 Filling the hole with x is correct, but it is not clear from the message
 that GHC knows this.
 It would be useful to have a section "Constraints include" e.g.

 {{{
 TypeEq.hs:5:19: error:
     Found hole: _ :: b
     Where: ‘b’ is a rigid type variable bound by
                the type signature for: castWith :: a :~: b -> a -> b
                at TypeEq.hs:4:13
     Relevant bindings include
       x :: a (bound at TypeEq.hs:5:15)
       castWith :: a :~: b -> a -> b (bound at TypeEq.hs:5:1)
     Constraints include                                        <------ NEW
 LINE
       a ~ b (from Refl :: a :~: a at TypeEq.hs:5:10)           <------ NEW
 LINE
     In the expression: _
     In an equation for ‘castWith’: castWith Refl x = _
 }}}

 And show class constraints (Show a etc.) similarly

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