[GHC] #15869: Discrepancy between seemingly equivalent type synonym and type family
#15869: Discrepancy between seemingly equivalent type synonym and type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.2 (Type checker) | Keywords: TypeFamilies | 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: -------------------------------------+------------------------------------- Consider the following code: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind type KindOf1 (a :: k) = k type family KindOf2 (a :: k) :: Type where KindOf2 (a :: k) = k data A (a :: Type) :: a -> Type type family Apply1 (f :: KindOf1 A) (a :: Type) (x :: a) :: Type where Apply1 f a x = f a x }}} `Apply1` kind-checks, which is just peachy. Note that `Apply1` uses `KindOf1`, which is a type synonym. Suppose I wanted to swap out `KindOf1` for `KindOf2`, which is (seemingly) an equivalent type family. I can define this: {{{#!hs type family Apply2 (f :: KindOf2 A) -- (f :: forall a -> a -> Type) (a :: Type) (x :: a) :: Type where Apply2 f a x = f a x }}} However, GHC rejects this! {{{ $ /opt/ghc/8.6.2/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:25:10: error: • Expecting two more arguments to ‘f’ Expected kind ‘KindOf2 A’, but ‘f’ has kind ‘* -> a -> *’ • In the first argument of ‘Apply2’, namely ‘f’ In the type family declaration for ‘Apply2’ | 25 | Apply2 f a x = f a x | ^ }}} I find this quite surprising, since I would have expected `KindOf1` and `KindOf2` to be functionally equivalent. Even providing explicit `forall`s does not make it kind-check: {{{#!hs type family Apply2 (f :: KindOf2 A) -- (f :: forall a -> a -> Type) (a :: Type) (x :: a) :: Type where forall (f :: KindOf2 A) (a :: Type) (x :: a). Apply2 f a x = f a x }}} Although the error message does change a bit: {{{ $ ~/Software/ghc3/inplace/bin/ghc-stage2 Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:26:20: error: • Expected kind ‘* -> a -> *’, but ‘f’ has kind ‘KindOf2 A’ • In the type ‘f a x’ In the type family declaration for ‘Apply2’ | 26 | Apply2 f a x = f a x | ^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15869 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15869: Discrepancy between seemingly equivalent type synonym and type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.6.2 checker) | Resolution: | Keywords: TypeFamilies 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): This isn't the only discrepancy I've encountered (although this is the most prominent example that I've uncovered). Another, slightly more minor discrepancy can be found in this program: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# OPTIONS_GHC -Wall -fprint-explicit-foralls #-} module Bug where import Data.Kind type KindOf1 (a :: k) = k type family KindOf2 (a :: k) :: Type where KindOf2 (a :: k) = k data A (a :: Type) :: a -> Type f :: KindOf1 A f = undefined g = f h = g }}} Compiling this yields the following warnings: {{{ $ /opt/ghc/8.6.2/bin/ghci Bug.hs GHCi, version 8.6.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:19:1: warning: [-Wmissing-signatures] Top-level binding with no type signature: g :: forall {a}. a -> * | 19 | g = f | ^ Bug.hs:20:1: warning: [-Wmissing-signatures] Top-level binding with no type signature: h :: forall {a}. a -> * | 20 | h = g | ^ }}} Note the inferred type signatures for `g` and `h` (Side note: it's a bit weird that their inferred types are `forall {a}. a -> *` and not, say, `forall a -> a -> *`. But that's not the main issue here.) Now, if you redefine `f` to use `KindOf2` in its type signature: {{{#!hs f :: KindOf2 A f = undefined }}} Recompiling the module will instead yield these warnings: {{{ $ /opt/ghc/8.6.2/bin/ghci Bug.hs GHCi, version 8.6.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:19:1: warning: [-Wmissing-signatures] Top-level binding with no type signature: g :: forall a -> a -> * | 19 | g = f | ^ Bug.hs:20:1: warning: [-Wmissing-signatures] Top-level binding with no type signature: h :: forall {a}. a -> * | 20 | h = g | ^ }}} Notice that the inferred type of `g` is now `forall a -> a -> *`, whereas before it was `forall {a}. a -> *`! Quite strange. (And to make things stranger, the inferred type of `h` is different from that of `g`.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15869#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15869: Discrepancy between seemingly equivalent type synonym and type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.6.2 checker) | Resolution: | Keywords: TypeFamilies 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 goldfire): Lots of bugs here! 1. I would expect `Apply1` to be rejected without an explicit `forall` in the equation, giving the polytype of `f`. 2. The error message for `Apply2` shouldn't say that it expects for arguments to `f`. The rest of the error message is perhaps confusing, but it's not unreasonable. 3. The version of `Apply2` with the explicit `forall` in the equation should be accepted. 4. In the `g` and `h` with `KindOf1`: Their types should be `forall a -> a -> Type`, not what GHC is reporting. 5. Ditto for `h` in the `KindOf2` case. Note that the inferred nature (as opposed to specified) of `a` is a non- bug: when you don't write a type signature, you don't get specified variables. But of course these should be required, not invisible or specified. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15869#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15869: Discrepancy between seemingly equivalent type synonym and type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.6.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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: TypeFamilies => TypeFamilies, TypeInType -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15869#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15869: Discrepancy between seemingly equivalent type synonym and type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.6.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: | -------------------------------------+------------------------------------- Description changed by RyanGlScott: Old description:
Consider the following code:
{{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-} module Bug where
import Data.Kind
type KindOf1 (a :: k) = k type family KindOf2 (a :: k) :: Type where KindOf2 (a :: k) = k
data A (a :: Type) :: a -> Type type family Apply1 (f :: KindOf1 A) (a :: Type) (x :: a) :: Type where Apply1 f a x = f a x }}}
`Apply1` kind-checks, which is just peachy. Note that `Apply1` uses `KindOf1`, which is a type synonym. Suppose I wanted to swap out `KindOf1` for `KindOf2`, which is (seemingly) an equivalent type family. I can define this:
{{{#!hs type family Apply2 (f :: KindOf2 A) -- (f :: forall a -> a -> Type) (a :: Type) (x :: a) :: Type where Apply2 f a x = f a x }}}
However, GHC rejects this!
{{{ $ /opt/ghc/8.6.2/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:25:10: error: • Expecting two more arguments to ‘f’ Expected kind ‘KindOf2 A’, but ‘f’ has kind ‘* -> a -> *’ • In the first argument of ‘Apply2’, namely ‘f’ In the type family declaration for ‘Apply2’ | 25 | Apply2 f a x = f a x | ^ }}}
I find this quite surprising, since I would have expected `KindOf1` and `KindOf2` to be functionally equivalent. Even providing explicit `forall`s does not make it kind-check:
{{{#!hs type family Apply2 (f :: KindOf2 A) -- (f :: forall a -> a -> Type) (a :: Type) (x :: a) :: Type where forall (f :: KindOf2 A) (a :: Type) (x :: a). Apply2 f a x = f a x }}}
Although the error message does change a bit:
{{{ $ ~/Software/ghc3/inplace/bin/ghc-stage2 Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:26:20: error: • Expected kind ‘* -> a -> *’, but ‘f’ has kind ‘KindOf2 A’ • In the type ‘f a x’ In the type family declaration for ‘Apply2’ | 26 | Apply2 f a x = f a x | ^^^^^ }}}
New description: Consider the following code: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE LiberalTypeSynonyms #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind type KindOf1 (a :: k) = k type family KindOf2 (a :: k) :: Type where KindOf2 (a :: k) = k data A (a :: Type) :: a -> Type type family Apply1 (f :: KindOf1 A) (a :: Type) (x :: a) :: Type where Apply1 f a x = f a x }}} `Apply1` kind-checks, which is just peachy. Note that `Apply1` uses `KindOf1`, which is a type synonym. Suppose I wanted to swap out `KindOf1` for `KindOf2`, which is (seemingly) an equivalent type family. I can define this: {{{#!hs type family Apply2 (f :: KindOf2 A) -- (f :: forall a -> a -> Type) (a :: Type) (x :: a) :: Type where Apply2 f a x = f a x }}} However, GHC rejects this! {{{ $ /opt/ghc/8.6.2/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:25:10: error: • Expecting two more arguments to ‘f’ Expected kind ‘KindOf2 A’, but ‘f’ has kind ‘* -> a -> *’ • In the first argument of ‘Apply2’, namely ‘f’ In the type family declaration for ‘Apply2’ | 25 | Apply2 f a x = f a x | ^ }}} I find this quite surprising, since I would have expected `KindOf1` and `KindOf2` to be functionally equivalent. Even providing explicit `forall`s does not make it kind-check: {{{#!hs type family Apply2 (f :: KindOf2 A) -- (f :: forall a -> a -> Type) (a :: Type) (x :: a) :: Type where forall (f :: KindOf2 A) (a :: Type) (x :: a). Apply2 f a x = f a x }}} Although the error message does change a bit: {{{ $ ~/Software/ghc3/inplace/bin/ghc-stage2 Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:26:20: error: • Expected kind ‘* -> a -> *’, but ‘f’ has kind ‘KindOf2 A’ • In the type ‘f a x’ In the type family declaration for ‘Apply2’ | 26 | Apply2 f a x = f a x | ^^^^^ }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15869#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15869: Discrepancy between seemingly equivalent type synonym and type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.6.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): While implementing visible dependent quantification (VDQ), I decided to revisit commment:2. Here are some of my findings: * I think (4) and (5) are ultimately non-issues, at least for the time being. This is because you won't be able to define `f` (or `g` or `h`) in the first place: {{{ Bug.hs:17:6: error: • Illegal visible, dependent quantification in the type of a term: forall a -> a -> * (GHC does not yet support this) • In the expansion of type synonym ‘KindOf1’ In the type signature: f :: KindOf1 A | 17 | f :: KindOf1 A | ^^^^^^^^^ }}} Since terms aren't meant to have types with VDQ in them, I don't think it's worth fretting over (4) and (5). Of course, if VDQ //does// ever become permitted in terms, perhaps this will pop back up. * (1) appears to be unrelated to VDQ and is actually a quirk of `ImpredicativeTypes`. Here is an example to illustrate what I mean: {{{#!hs {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} module Bug where import Data.Kind type family F (f :: forall a. a -> Type) where F f = f Int }}} This doesn't typecheck: {{{ Bug.hs:9:5: error: • Expected kind ‘forall a. a -> *’, but ‘f’ has kind ‘* -> k0’ • In the first argument of ‘F’, namely ‘f’ In the type family declaration for ‘F’ | 9 | F f = f Int | ^ }}} However, if you enable `ImpredicativeTypes`, then it //does// typecheck! It's unclear to me why exactly that is, however. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15869#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15869: Discrepancy between seemingly equivalent type synonym and type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.6.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 simonpj): If you don't have impredicative-types, then surely the example in the second bullet of comment:5 should be rejected! But still, the error message looks deeply strange. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15869#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15869: Discrepancy between seemingly equivalent type synonym and type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.6.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): To be clear, I am in agreement with you that the program in the second bullet point of comment:5 should be rejected if `ImpredicativeTypes` is not enabled. I am simply wondering if it being accepted //with// `ImpredicativeTypes` enabled should count as a bug in its own right. (It's such a squirrelly extension that I can never tell whether it's working as intended or not.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15869#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15869: Discrepancy between seemingly equivalent type synonym and type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.6.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): (2) might also be its own issue, since you can trigger the "expecting more arguments" error without VDQ: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeFamilies #-} module Bug where type family F type family G (f :: F) where G f = f Int }}} {{{ $ /opt/ghc/8.6.3/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:8:5: error: • Expecting one more argument to ‘f’ Expected kind ‘F’, but ‘f’ has kind ‘* -> k0’ • In the first argument of ‘G’, namely ‘f’ In the type family declaration for ‘G’ | 8 | G f = f Int | ^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15869#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15869: Discrepancy between seemingly equivalent type synonym and type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.6.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): I wonder if (3) has anything to do with #9269? `KindOf2 A` is a bit weird in that it's an application of a type family that returns `forall a -> a -> Type`, which is a polymorphic type. Normally, GHC disallows that—you wouldn't be able to define `type family FAA where FAA = forall a -> a -> Type`, for instance. Yet `KindOf2` offers a way around this restriction, so perhaps (3) is a manifestation of GHC trying to deal with something it doesn't know how to reason about. Then again, `KindOf2 A` seems to work in other places, as comment:1 demonstrates. It's just in type family equations where things go haywire. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15869#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15869: Discrepancy between seemingly equivalent type synonym and type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.6.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): It's entirely possible that (2) is actually a duplicate of #14319, especially in light of comment:8. (Then again, it's not clear why `KindOf2 A` isn't reducing in that type family equation in the first place—see comment:9.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15869#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15869: Discrepancy between seemingly equivalent type synonym and type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.6.2 checker) | Keywords: TypeFamilies, Resolution: | TypeInType, | VisibleDependentQuantification 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: TypeFamilies, TypeInType => TypeFamilies, TypeInType, VisibleDependentQuantification -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15869#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC