[GHC] #14045: Data family instances must list all patterns of family, despite documentation's claims to the contrary
#14045: Data family instances must list all patterns of family, despite documentation's claims to the contrary -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 (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: #12369 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- (Originally spun off from #12369.) The documentation for data families currently [http://git.haskell.org/ghc.git/blob/791947db6db32ef7d4772a821a0823e558e3c05b... claims]: {{{ - Data families have been generalised a bit: a data family declaration can now end with a kind variable ``k`` instead of ``Type``. Additionally, data/newtype instance no longer need to list all the patterns of the family if they don't wish to; this is quite like how regular datatypes with a kind signature can omit some type variables. }}} Moreover, the commit which added this (4239238306e911803bf61fdda3ad356fd0b42e05) cites this particular example: {{{#!hs data family Sing (a :: k) data instance Sing :: Bool -> Type where ... }}} However, in practice, this does //not// typecheck on GHC HEAD: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} import Data.Kind data family Sing (a :: k) data instance Sing :: Bool -> Type where SFalse :: Sing False STrue :: Sing True }}} {{{ $ ~/Software/ghc5/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.3.20170725: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Main ( Bug.hs, interpreted ) Bug.hs:8:1: error: • Number of parameters must match family declaration; expected 0 • In the data instance declaration for ‘Sing’ | 8 | data instance Sing :: Bool -> Type where | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^... }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14045 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14045: Data family instances must list all patterns of family, despite documentation's claims to the contrary -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.3 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: #12369 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * cc: Iceland_jack (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14045#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14045: Data family instances must list all patterns of family, despite documentation's claims to the contrary -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.3 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: #12369 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Similarly, associated data family instances of this form are also rejected: {{{#!hs {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} import Data.Kind class C (a :: k) where data Sing (a :: k) instance C (z :: Bool) where data Sing :: Bool -> Type where SFalse :: Sing False STrue :: Sing True }}} {{{ $ ~/Software/ghc5/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.3.20170725: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Main ( Bug.hs, interpreted ) Bug.hs:12:3: error: • Number of parameters must match family declaration; expected 0 • In the data instance declaration for ‘Sing’ In the instance declaration for ‘C (z :: Bool)’ | 12 | data Sing :: Bool -> Type where | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^... }}} I'm not sure if such a thing would be permissible, since GHC imposes some [http://git.haskell.org/ghc.git/blob/791947db6db32ef7d4772a821a0823e558e3c05b... additional restrictions] on the type patterns of associated family instances. If it's not permissible, we should give a better error message here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14045#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14045: Data family instances must list all patterns of family, despite documentation's claims to the contrary -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.3 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: #12369 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * cc: goldfire (added) Comment: To me the `k` argument to `Sing` looks like an invisible (implicit) one. So you should need visible kind application to use it in an invocation, something like {{{ instance C (z :: Bool) where data Sing :: Bool -> Type where SFalse :: Sing @False STrue :: Sing @True }}} Let's see what Richard says. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14045#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14045: Data family instances must list all patterns of family, despite documentation's claims to the contrary -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.3 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: #12369 | Differential Rev(s): Phab:D3804 Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * differential: => Phab:D3804 Comment: Well, that's embarrassing. Easy enough to fix, but annoying to get good error messages in the mismatched associated type case (comment:2, which I think should be rejected). I'm afraid I think comment:3 is in error -- I don't understand what you're getting at. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14045#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14045: Data family instances must list all patterns of family, despite
documentation's claims to the contrary
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type | Version: 8.3
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: #12369 | Differential Rev(s): Phab:D3804
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg
#14045: Data family instances must list all patterns of family, despite documentation's claims to the contrary -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.3 checker) | Resolution: fixed | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T14045, | indexed-types/should_fail/T14045a Blocked By: | Blocking: Related Tickets: #12369 | Differential Rev(s): Phab:D3804 Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => closed * testcase: => indexed-types/should_compile/T14045, indexed- types/should_fail/T14045a * resolution: => fixed Comment: All set now. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14045#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14045: Data family instances must list all patterns of family, despite documentation's claims to the contrary -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.3 checker) | Resolution: fixed | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T14045, | indexed-types/should_fail/T14045a Blocked By: | Blocking: Related Tickets: #12369 | Differential Rev(s): Phab:D3804 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I don't see in the patch where an arity check is omitted. And I'd love a Note somewhere giving examples of "Data families aren't as particular about their arity as type families are (because data families can be undersaturated)", at some relevant point in the type checker. The point is, I guess, that {{{ data instance Sing :: Bool -> Type where SFalse :: Sing False STrue :: Sing True }}} and {{{ data instance Sing (a :: Bool) :: Type where SFalse :: Sing False STrue :: Sing True }}} are similar, but not quite the same. Moreover, different instances can make different choices. Moreover you can't to that for type families. We should call that out somewhere, and explain why it's different (data families can be decomposed, type families can't). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14045#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14045: Data family instances must list all patterns of family, despite documentation's claims to the contrary -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.3 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T14045, | indexed-types/should_fail/T14045a Blocked By: | Blocking: Related Tickets: #12369 | Differential Rev(s): Phab:D3804 Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: closed => new * resolution: fixed => -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14045#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14045: Data family instances must list all patterns of family, despite
documentation's claims to the contrary
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type | Version: 8.3
checker) |
Resolution: | Keywords: TypeFamilies
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: GHC rejects | Test Case: indexed-
valid program | types/should_compile/T14045,
| indexed-types/should_fail/T14045a
Blocked By: | Blocking:
Related Tickets: #12369 | Differential Rev(s): Phab:D3804
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg
#14045: Data family instances must list all patterns of family, despite documentation's claims to the contrary -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.3 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T14045, | indexed-types/should_fail/T14045a Blocked By: | Blocking: Related Tickets: #12369 | Differential Rev(s): Phab:D3804 Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Does that do it? It's all in `Note [Arity of data families]` in FamInstEnv. Also, the skipped arity check in the previous patch is in `tc_fam_ty_pats` in TcTyClsDecls. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14045#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14045: Data family instances must list all patterns of family, despite documentation's claims to the contrary -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.3 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T14045, | indexed-types/should_fail/T14045a Blocked By: | Blocking: Related Tickets: #12369 | Differential Rev(s): Phab:D3804 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Ah I missed the reference to `Note [Arity of data families]`. Thanks. But {{{ This instance is very nearly equivalent to data instance Sing (a :: Bool) where ... but without the last pattern, we have an under-saturated data family instance. On its own, this example is not compelling }}} Can you say more precisely what /is/ the difference? Is it only the newtype-eta thing? Or is there anything else? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14045#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14045: Data family instances must list all patterns of family, despite documentation's claims to the contrary -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.3 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T14045, | indexed-types/should_fail/T14045a Blocked By: | Blocking: Related Tickets: #12369 | Differential Rev(s): Phab:D3804 Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): There isn't a difference. {{{#!hs data instance Sing (a :: Bool) where ... }}} and {{{#!hs data instance Sing :: Bool -> Type where ... }}} compile to precisely the same internal representation. It's the same because the first one gets eta-reduced to look like the second. That's why the note says {{{ This instance is equivalent to `data instance Sing (a :: Bool)` }}} I'm not sure where you get "very nearly equivalent" above. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14045#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14045: Data family instances must list all patterns of family, despite documentation's claims to the contrary -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.3 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T14045, | indexed-types/should_fail/T14045a Blocked By: | Blocking: Related Tickets: #12369 | Differential Rev(s): Phab:D3804 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Yes, you're right. What I should have said is this. There is no reason to allow data instances to be written under-saturated. That is, we could insist on {{{ data instance Sing (a :: Bool) where ... }}} But, as an additional feature, we allow you to drop any trailing patterns that are simply type variables (if not mentioned earlier). Thus {{{ data instance T Int [a] (c::*) (d::Bool) (e::*) where ... }}} can also be written equivalently {{{ data instance T Int [a] :: * -> Bool -> * -> * where ... }}} Is that right? If so, let's update the user manual to say so. Alas, we have a bug, I think. Consider {{{ data family T a b :: Type newtype instance T Int :: Type -> Type where MkT :: IO a -> T Int a deriving( Monad, Applicative, Functor ) }}} Oddly, this fails with {{{ Foo2.hs:38:13: error: • Can't make a derived instance of ‘Monad (T Int)’ (even with cunning GeneralizedNewtypeDeriving): cannot eta-reduce the representation type enough }}} Whereas this succeeds {{{ newtype instance T Int a :: Type where MkT :: IO a -> T Int a deriving( Monad, Applicative, Functor ) }}} so the two aren't (yet) quite equivalent. Do you agree this is a bug? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14045#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14045: Data family instances must list all patterns of family, despite documentation's claims to the contrary -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.3 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T14045, | indexed-types/should_fail/T14045a Blocked By: | Blocking: Related Tickets: #12369 | Differential Rev(s): Phab:D3804 Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott):
Do you agree this is a bug?
I certainly do. In the bowels of `TcDeriv`, we check that `newTyConEtadRhs` (the eta-reduced representation type) can accommodate the number of arguments from the instance we're deriving. But after doing some `pprTrace` scavenging, I discovered that the `newTyConEtadRhs` for `newtype instance T Int :: Type -> Type` is {{{#!hs ([a_a1vc], IO a_a1vc) }}} Whereas for `newtype instance T Int a :: Type`, it's: {{{#!hs ([], IO) }}} Something fishy is going on. The result of `newTyConEtadRhs` is ultimately being created in `mkNewTyConRhs`, which computes the eta-reduced type variables by checking one-by-one if a tycon tyvar matches the tyvar in the representation type in the corresponding position (see [https://git.haskell.org/ghc.git/blob/c13720c8c6047844f659ad4ce684946b80c99be... eta_reduce]). My guess is that this `a_a1vc` tyvar from the representation type doesn't match the corresponding tyvar from `newtype instance T Int :: Type -> Type` (what //would// the corresponding tyvar be, anyway?) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14045#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14045: Data family instances must list all patterns of family, despite documentation's claims to the contrary -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.3 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T14045, | indexed-types/should_fail/T14045a Blocked By: | Blocking: Related Tickets: #12369 | Differential Rev(s): Phab:D3804 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I found it. Patch coming. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14045#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14045: Data family instances must list all patterns of family, despite
documentation's claims to the contrary
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type | Version: 8.3
checker) |
Resolution: | Keywords: TypeFamilies
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: GHC rejects | Test Case: indexed-
valid program | types/should_compile/T14045,
| indexed-types/should_fail/T14045a
Blocked By: | Blocking:
Related Tickets: #12369 | Differential Rev(s): Phab:D3804
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by simonpj):
I ran out of time, got stuck upgrading to GHC 8 which is now required...
Here is the patch: Ryan, would you like to validate and commit?
{{{
simonpj@cam-05-unx:~/code/HEAD$ git show 143f08a3
commit 143f08a32b80f7f80d77b518ce207a1051368b9e
Author: Simon Peyton Jones
#14045: Data family instances must list all patterns of family, despite
documentation's claims to the contrary
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type | Version: 8.3
checker) |
Resolution: | Keywords: TypeFamilies
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: GHC rejects | Test Case: indexed-
valid program | types/should_compile/T14045,
| indexed-types/should_fail/T14045a
Blocked By: | Blocking:
Related Tickets: #12369 | Differential Rev(s): Phab:D3804
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ryan Scott
#14045: Data family instances must list all patterns of family, despite documentation's claims to the contrary -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.3 checker) | Resolution: fixed | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T14045, | indexed-types/should_fail/T14045a, | deriving/should_compile/T14045b Blocked By: | Blocking: Related Tickets: #12369 | Differential Rev(s): Phab:D3804 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * testcase: indexed-types/should_compile/T14045, indexed- types/should_fail/T14045a => indexed-types/should_compile/T14045, indexed- types/should_fail/T14045a, deriving/should_compile/T14045b * resolution: => fixed Comment: Done. Thanks, Simon! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14045#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC