GitLab

This works

{-# Language RankNTypes, PolyKinds, GADTs #-}

newtype Nat :: (k -> *) -> (k -> *) -> * where
  Nat :: (forall xx. f xx -> g xx) -> Nat f g

but this

{-# Language RankNTypes, PolyKinds, GADTs, TypeFamilies #-}

data family Nat :: k -> k -> *

newtype instance Nat :: (k -> *) -> (k -> *) -> * where
  Nat :: (forall xx. f xx -> g xx) -> Nat f g

fails on GHC 8.3.20170815, and requires a forall k. to work

$ ./ghc-stage2 -ignore-dot-ghci --interactive /tmp/kind.hs 
GHCi, version 8.3.20170815: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( /tmp/kind.hs, interpreted )

/tmp/kind.hs:5:26: error: Not in scope: type variable ‘k’
  |
5 | newtype instance Nat :: (k -> *) -> (k -> *) -> * where
  |                          ^

/tmp/kind.hs:5:38: error: Not in scope: type variable ‘k’
  |
5 | newtype instance Nat :: (k -> *) -> (k -> *) -> * where
  |                                      ^
Failed, 0 modules loaded.

Related to #12369 (closed)?

Trac metadata

Trac field	Value
Version	8.2.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture