[GHC] #11192: Induced `Eq` constraint on numeric literal + partial type signature = panic!

10 Dec 2015

      #11192: Induced `Eq` constraint on numeric literal + partial type signature =
panic!
-------------------------------------+-------------------------------------
           Reporter:  kwf            |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  7.10.2
  (Type checker)                     |
           Keywords:  numeric        |  Operating System:  Unknown/Multiple
  literal, partial type signature,   |
  the impossible happened, panic     |
       Architecture:                 |   Type of failure:  Compile-time
  Unknown/Multiple                   |  crash
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 When I use a partial type signature in a non-top-level let-binding (or
 where clause), ''and'' the type is sufficiently ambiguous, ''and'' the
 binding in question uses a numeric literal, I get a panic from GHC instead
 of a report of the inferred type of the hole.

 So, this breaks:

 {{{#!hs
 module Fails where

 fails :: a
 fails =
    let go :: _
        go 0 a = a
    in go (0 :: Int) undefined
 }}}

 {{{
 Fails.hs:7:11:
     Couldn't match expected type ‘a’ with actual type ‘Int’
       ‘a’ is untouchable
         inside the constraints ()
         bound by the type signature for fails :: a1
         at Fails.hs:3:10ghc: panic! (the 'impossible' happened)
   (GHC version 7.10.2 for x86_64-apple-darwin):
    No skolem info: a_a1iD[sk]
 }}}

 ...but this succeeds:

 {{{#!hs
 module Succeeds where

 succeeds :: a
 succeeds =
    let go :: _
        go _ a = a
    in go (0 :: Int) undefined
 }}}

 {{{
 Succeeds.hs:13:14:
     Found hole ‘_’ with type: t -> t1 -> t1
     Where: ‘t’ is a rigid type variable bound by
                the inferred type of go :: t -> t1 -> t1 at
 Succeeds.hs:14:8
            ‘t1’ is a rigid type variable bound by
                 the inferred type of go :: t -> t1 -> t1 at
 Succeeds.hs:14:8
     To use the inferred type, enable PartialTypeSignatures
     <snip>
 }}}

 The '''only''' difference between these two modules is the use of a
 numeric literal in a pattern match; that is, the troublesome line boils
 down to:

 {{{#!hs
 go 0 a = a
 }}}

 vs.

 {{{#!hs
 go _ a = a
 }}}

 Note that GHC gives us several pieces of feedback before talking about the
 panic. Before the above-quoted error, we get:

 {{{
 Fails.hs:5:14:
     Found hole ‘_’ with type: a2 -> t1 -> t1
     Where: ‘t1’ is a rigid type variable bound by
                 the inferred type of go :: (Eq a2, Num a2) => a2 -> t1 ->
 t1
                 at Fails.hs:6:8
            ‘a2’ is a rigid type variable bound by
                 the inferred type of go :: (Eq a2, Num a2) => a2 -> t1 ->
 t1
                 at Fails.hs:6:8
     To use the inferred type, enable PartialTypeSignatures
     <snip>

 Fails.hs:6:8:
     No instance for (Eq a)
     When checking that ‘go’ has the specified type
       go :: forall t a. a -> t -> t
     Probable cause: the inferred type is ambiguous
     <snip>

 Fails.hs:7:7:
     Couldn't match expected type ‘a1’ with actual type ‘t’
       because type variable ‘a1’ would escape its scope
     This (rigid, skolem) type variable is bound by
       the type signature for fails :: a1
       at Fails.hs:3:10
     <snip>
 }}}

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