Type of hole does not get refined after pattern matching on [GADT] constructors
From A Practical Introduction to Haskell GADTs from LambdaConf 2015, example from attachment Hole.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?
Trac metadata
Trac field | Value |
---|---|
Version | 7.11 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |