GADTs don't refine hole types

Apologies if this is a dupe. I did look!

{-# LANGUAGE GADTs #-}

data T a where
    I :: T Int

f :: T a -> a
f I = _

This gives the type error:

    • Found hole: _ :: a
      Where: ‘a’ is a rigid type variable bound by
               the type signature for:
                 f :: forall a. T a -> a
               at test.hs:6:6
    • In the expression: _
      In an equation for ‘f’: f I = _
    • Relevant bindings include f :: T a -> a (bound at test.hs:7:1)

It should say something about a being Int in this branch.

I'm using GHC 8.0.1 on OSX El Capitan. I think this may be a regression; I have a vague memory of it working with GHC 7.10.

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system	MacOS X
Architecture