#14887: Explicitly quantifying a kind variable causes a type family to fail to typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.2 checker) | Keywords: TypeFamilies, Resolution: | TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): A slight twist on this is if you leave out the type family equations. For instance: {{{#!hs {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# OPTIONS_GHC -fprint-explicit-kinds #-} module Bug where import Data.Kind import Data.Proxy type family Foo1 (e :: Proxy (a :: k)) :: Type where {} type family Foo2 (k :: Type) (e :: Proxy (a :: k)) :: Type where {} }}} `Foo1` typechecks, but `Foo2` does not: {{{ $ ghci Bug.hs -fprint-explicit-kinds GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:10:1: error: • These kind and type variables: k (e :: Proxy k a) are out of dependency order. Perhaps try this ordering: k (a :: k) (e :: Proxy k a) NB: Implicitly declared kind variables are put first. • In the type family declaration for ‘Foo2’ | 10 | type family Foo2 (k :: Type) (e :: Proxy (a :: k)) :: Type where {} | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} I have no idea why GHC is complaining about the scoping order here—that looks well-scoped to me! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14887#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler