Skip to content

GitLab

Closed
Opened by Ryan Scott@RyanGlScottMaintainer

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
Edited by Ryan Scott