[GHC] #11325: Type of hole does not get refined after pattern matching on [GADT] constructors

31 Dec 2015

      #11325: Type of hole does not get refined after pattern matching on [GADT]
constructors
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  7.11
  (Type checker)                     |
           Keywords:  GADTs          |  Operating System:  Linux
       Architecture:  x86            |   Type of failure:  Incorrect
                                     |  warning at compile-time
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 From [https://www.youtube.com/watch?v=6snteFntvjM A Practical Introduction
 to Haskell GADTs] from LambdaConf 2015, example from attachment Hole.hs:

 {{{#!hs
 {-# LANGUAGE GADTs #-}

 data STy ty where
   SInt   :: STy Int
   SBool  :: STy Bool
   SMaybe :: STy a -> STy (Maybe a)

 zero :: STy ty -> ty
 zero ty = case ty of
   SInt     -> 5
   SBool    -> False
   SMaybe a -> _
 }}}

 When running with "GHCi, version 7.11.20151226":

 {{{
 % ghci -ignore-dot-ghci /tmp/Hole.hs
 GHCi, version 7.11.20151226: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Main             ( /tmp/Hole.hs, interpreted )

 /tmp/Hole.hs:12:15: error:
     • Found hole: _ :: ty
       Where: ‘ty’ is a rigid type variable bound by
                the type signature for:
                  zero :: forall ty. STy ty -> ty
                at /tmp/Hole.hs:8:9
     • In the expression: _
       In a case alternative: SMaybe a -> _
       In the expression:
         case ty of {
           SInt -> 5
           SBool -> False
           SMaybe a -> _ }
     • Relevant bindings include
         a :: STy a (bound at /tmp/Hole.hs:12:10)
         ty :: STy ty (bound at /tmp/Hole.hs:9:6)
         zero :: STy ty -> ty (bound at /tmp/Hole.hs:9:1)
 Failed, modules loaded: none.
 Prelude>
 }}}

 when older versions (GHCi version 7.10.2) refine the type of `_` to `Maybe
 a`:

 {{{
 % ghci-7.10.2 -ignore-dot-ghci /tmp/Hole.hs
 GHCi, version 7.10.2: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Main             ( /tmp/Hole.hs, interpreted )

 /tmp/Hole.hs:12:15:
     Found hole ‘_’ with type: Maybe a
     Where: ‘a’ is a rigid type variable bound by
                a pattern with constructor
                  SMaybe :: forall a. STy a -> STy (Maybe a),
                in a case alternative
                at /tmp/Hole.hs:12:3
     Relevant bindings include
       a :: STy a (bound at /tmp/Hole.hs:12:10)
       ty :: STy ty (bound at /tmp/Hole.hs:9:6)
       zero :: STy ty -> ty (bound at /tmp/Hole.hs:9:1)
     In the expression: _
     In a case alternative: SMaybe a -> _
     In the expression:
       case ty of {
         SInt -> 5
         SBool -> False
         SMaybe a -> _ }
 Failed, modules loaded: none.
 Prelude>
 }}}

 Regression?

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