[GHC] #14515: "Same" higher-rank kind synonyms behave differently
#14515: "Same" higher-rank kind synonyms behave differently -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- As you know type-level `forall`s don't float, so we may want to write `HRefl`'s kind {{{#!hs -- Different from -- HREFL :: forall k1 k2. k1 -> k2 -> Type -- data HREFL :: forall k1. k1 -> (forall k2. k2 -> Type) where HREFL :: HREFL a a }}} Let us capture `forall k2. k2 -> ..` with a kind synonym {{{#!hs type HRank2 ty = forall k2. k2 -> ty data HREFL :: forall k. k -> HRank2 Type where HREFL :: HREFL a a }}} Works fine. Phew. Let's do the same for `forall k1. k1 -> ..` {{{#!hs type HRank1 ty = forall k1. k1 -> ty type HRank2 ty = forall k2. k2 -> ty data HREFL :: HRank1 (HRank2 Type) where HREFL :: HREFL a a }}} Works fine. Phew. “Didn't you just define the same kind synonym twice?” The funny thing is that this fails to compile when they coincide! {{{#!hs data HREFL :: HRank1 (HRank1 Type) -- FAILS data HREFL :: HRank1 (HRank2 Type) -- OK data HREFL :: HRank2 (HRank1 Type) -- OK data HREFL :: HRank2 (HRank2 Type) -- FAILS }}} {{{ $ ghci -ignore-dot-ghci /tmp/Weird.hs GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( /tmp/Weird.hs, interpreted ) /tmp/Weird.hs:8:1: error: • These kind and type variables: (b :: k2) k2 (d :: k2) are out of dependency order. Perhaps try this ordering: k2 (b :: k2) (d :: k2) • In the data type declaration for ‘HREFL’ | 8 | data HREFL :: HRank2 (HRank2 Type) | ^^^^^^^^^^ Failed, 0 modules loaded. Prelude> }}} Same happens defining `HRank2` in terms of `HRank1` {{{#!hs type HRank1 ty = forall k1. k1 -> ty type HRank2 ty = HRank1 ty }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14515 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14515: "Same" higher-rank kind synonyms behave differently -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: 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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: => TypeInType * failure: None/Unknown => GHC rejects valid program * component: Compiler => Compiler (Type checker) Comment: For the sake of convenience, here's all of the various combinations in one file: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind type HRank1 ty = forall k1. k1 -> ty type HRank2 ty = forall k2. k2 -> ty data HREFL11 :: HRank1 (HRank1 Type) where HREFL11 :: HREFL11 a a data HREFL12 :: HRank1 (HRank2 Type) where HREFL12 :: HREFL12 a a data HREFL21 :: HRank2 (HRank1 Type) where HREFL21 :: HREFL21 a a data HREFL22 :: HRank2 (HRank2 Type) where HREFL22 :: HREFL22 a a }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14515#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14515: "Same" higher-rank kind synonyms behave differently -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: 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 Iceland_jack): The constructor isn't necessary to trigger it {{{#!hs {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind type HRank1 ty = forall k1. k1 -> ty type HRank2 ty = forall k2. k2 -> ty data HREFL11 :: HRank1 (HRank1 Type) -- FAILS data HREFL12 :: HRank1 (HRank2 Type) data HREFL21 :: HRank2 (HRank1 Type) data HREFL22 :: HRank2 (HRank2 Type) -- FAILS }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14515#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14515: "Same" higher-rank kind synonyms behave differently
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: (none)
Type: bug | Status: closed
Priority: normal | Milestone:
Component: Compiler (Type | Version: 8.2.1
checker) |
Resolution: fixed | Keywords: TypeInType
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: GHC rejects | Test Case:
valid program | polykinds/T14515
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Changes (by simonpj):
* status: new => closed
* testcase: => polykinds/T14515
* resolution: => fixed
Comment:
Great examples! Fixed by
{{{
commit 68149452a793aedd8d468b689dc93fb2ba5ec436
Author: Simon Peyton Jones
---------------------------------------------------------------
68149452a793aedd8d468b689dc93fb2ba5ec436 compiler/typecheck/TcHsType.hs | 126 +++++++++++++++++------------ compiler/typecheck/TcInstDcls.hs | 20 ++--- compiler/typecheck/TcTyClsDecls.hs | 22 +++-- compiler/types/Type.hs | 16 +--- testsuite/tests/ghci/scripts/T13407.stdout | 2 +- testsuite/tests/polykinds/T14515.hs | 13 +++ testsuite/tests/polykinds/all.T | 1 + 7 files changed, 116 insertions(+), 84 deletions(-) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14515#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC