[GHC] #16110: Explicit foralls in associated type family defaults are completely ignored?
#16110: Explicit foralls in associated type family defaults are completely ignored? -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.7 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC accepts Unknown/Multiple | invalid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- While playing around with GHC HEAD recently, I noticed some rather bizarre behavior when trying to use explicit `forall`s with associated type family defaults. Let's pop open GHCi and recreate it: {{{ $ inplace/bin/ghc-stage2 --interactive -XTypeFamilies -XScopedTypeVariables GHCi, version 8.7.20181215: https://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci λ> class C a where { type T a b; type forall b. T a b = Either a b } }}} OK, so far, so good. Now let's see what happens when I omit the `b`: {{{ λ> class C a where { type T a b; type forall. T a b = Either a b } }}} That... works? Wow, I wouldn't have expected that... But it gets even worse—I can type in utter nonsense, and GHCi will accept it: {{{ λ> class C a where { type T a b; type forall dup dup dup. T a b = Either a b } λ> class C a where { type T a b; type forall (a :: a). T a b = Either a b } λ> class C a where { type T a b; type forall (a :: k) k. T a b = Either a b } }}} How could this possibly happen? After looking at the source code to see how associated type family defaults are renamed, it becomes clear why this is the case. Here is how they are [http://git.haskell.org/ghc.git/blob/ef57272e28f5047599249ae457609a079d8aebef... renamed]: {{{#!hs rnTyFamDefltEqn cls (FamEqn { ... , feqn_bndrs = bndrs , ... }) = do { ... ; return (FamEqn { ... , feqn_bndrs = ASSERT( isNothing bndrs ) Nothing , ... }, ...) } }}} Not only are the type variable binders ignored, there's actually an `ASSERT`ion in place which assumes that there will be no binders whatsoever! (I haven't checked, but I suspect the code above will trigger a failure on that `ASSERT`ion.) My questions after seeing all of this are: * Should we be accepting explicit `forall`s in associated type family defaults at all? * If so, should we remove this strange invariant that the binders will always be `Nothing`? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16110 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16110: Explicit foralls in associated type family defaults are completely ignored? -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * cc: mayac (added) Comment: Cc'ing the author of the new feature. Matt? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16110#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16110: Explicit foralls in associated type family defaults are completely ignored? -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Slightly tangential question: why do type family defaults need type variable binders in the first place? After all, the arguments in a type family default must always be type variables anyway—if you try otherwise: {{{#!hs class C a where type T a type T Int = Int }}} Then GHC will just reject it: {{{ Unexpected type ‘Int’ In the default declaration for ‘T’ A default declaration should have form default T a = ... }}} (That error message is a bit skeevy, since you're not supposed to put the word "`default`" at the front like that. But that's a separate issue.) Given that type family default arguments are required to be all type variables anyway, does it really benefit us to have an explicit `forall` to bind them? (We don't do this for data, class, or type family declarations, for instance.) Or am I missing something obvious? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16110#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16110: Explicit foralls in associated type family defaults are completely ignored? -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Am I correct in believing that this change was part of implementing the [https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0007 -instance-foralls.rst explicit foralls GHC proposal]? (Incidentally, this proposal is not listed as "implemented" in [https://github.com/ghc-proposals/ghc- proposals/pulls?page=2&q=label%3AAcceptedthe main list]. Should it be?) The proposal is silent on whether it applies to default family instance decls. It'd be good to update the proposal to be clear on this point, since it is teh only specification we have. If the goal is to be able to explicitly bind every variable, would we need a forall for a default family instance? {{{ class C a where type T a b :: * type T a b = (a, [b]) }} Does the default instance need to replicate the type family signature? Eg can I say this? {{{ class C a where type T a b :: * type T x y = (x, [y]) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16110#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16110: Explicit foralls in associated type family defaults are completely ignored? -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): You can say the last example in comment:3, but you both raise a good question. Do we need these at all? While the variables in the default equation can alpha-vary from other places (I forget why we decided to allow that), they must be bare variables, of the right kinds. So we really know their kinds from the type family declaration. There is no need to be able to write their kinds in the default equation. So perhaps the best way forward is just to remove the featurette. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16110#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16110: Explicit foralls in associated type family defaults are completely ignored? -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Regardless, yes, we should update the proposal. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16110#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
So we really know their kinds from the type family declaration. There is no need to be able to write their kinds in the default equation. So
#16110: Explicit foralls in associated type family defaults are completely ignored? -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): perhaps the best way forward is just to remove the featurette. I agree. And let's update the proposal to match. We should also document whatever we decide (including the alpha-varying bit) in the user manual -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16110#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16110: Explicit foralls in associated type family defaults are completely ignored? -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I wonder: will we need to change some Template Haskell conventions to support this change? Currently, this: {{{#!hs [d| class C a where type T a type T a = a |] }}} Turns into this: {{{#!hs [ ClassD [] C_6989586621679039759 [ PlainTV a_6989586621679039761 ] [] [ OpenTypeFamilyD (TypeFamilyHead T_6989586621679039760 [ PlainTV a_6989586621679039761 ] NoSig Nothing) , TySynInstD (TySynEqn Nothing (AppT (ConT T_6989586621679039760) (VarT a_6989586621679039762)) (VarT a_6989586621679039762)) ] ] }}} Notice that we're using a `TySynInstD`/`TySynEqn` to represent the type family default, complete with a `Nothing` for its type variable binders. If we pursue the line of thought in this ticket, wouldn't that suggest that we should be using something else to represent this default? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16110#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16110: Explicit foralls in associated type family defaults are completely ignored? -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Not necessarily. We could always just check during conversion that there are no binders for type family defaults. I don't think it's a big deal. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16110#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC