Explicitly quantifying a kind variable causes a telescope to fail to kind-check
Consider the following program:
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fprint-explicit-kinds #-}
module Bug where
import Data.Kind
import Data.Type.Equality
type family Foo1 (e :: (a :: k) :~: (a :: k)) :: Type where
Foo1 (e :: a :~: a) = a :~: a
type family Foo2 (k :: Type) (e :: (a :: k) :~: (a :: k)) :: Type where
Foo2 k (e :: a :~: a) = a :~: a
Foo2
is wholly equivalent to Foo1
, except that in Foo2
, the k
kind variable is explicitly quantified. However, Foo1
typechecks, but Foo2
does not!
$ /opt/ghc/8.2.2/bin/ghci Bug.hs -fprint-explicit-kinds
GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/ryanglscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:13:10: error:
• Couldn't match kind ‘k’ with ‘k1’
When matching the kind of ‘a’
Expected kind ‘(:~:) k a a’, but ‘e’ has kind ‘(:~:) k a a’
• In the second argument of ‘Foo2’, namely ‘(e :: a :~: a)’
In the type family declaration for ‘Foo2’
|
13 | Foo2 k (e :: a :~: a) = a :~: a
| ^^^^^^^^^^^^^^
(Moreover, there seems to be a tidying bug, since GHC claims that (:~:) k a a
is not the same kind as (:~:) k a a
.)
Trac metadata
Trac field | Value |
---|---|
Version | 8.2.2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |