gadt-holes.hs

-- similar to https://ghc.haskell.org/trac/ghc/ticket/12468
-- except that I'm trying with 8.2.1

GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Prelude> :set -XGADTs
Prelude> data Foo a where Foo :: Int -> Foo Bool
Prelude> f :: Foo a -> a ; f (Foo n) = _k n

<interactive>:3:31: error:
    • Found hole: _k :: Int -> a
      Where: ‘a’ is a rigid type variable bound by
               the type signature for:
                 f :: forall a. Foo a -> a
               at <interactive>:3:1-15
      Or perhaps ‘_k’ is mis-spelled, or not in scope
    • In the expression: _k
      In the expression: _k n
      In an equation for ‘f’: f (Foo n) = _k n
    • Relevant bindings include
        n :: Int (bound at <interactive>:3:26)
        f :: Foo a -> a (bound at <interactive>:3:19)

-- I was expecting that the a ~ Int equality would be in scope when
-- typechecking the hole _k, therefore _k :: Int -> Bool.