[GHC] #15828: Type family equation foralls allow strange re-quantification of class-bound type variables
#15828: Type family equation foralls allow strange re-quantification of class-bound type variables -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.7 Keywords: TypeFamilies | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The following code typechecks on GHC HEAD (8.7+): {{{#!hs {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} module Bug where import Data.Kind class C1 a where type T1 a b class C2 a where type T2 a b instance C1 (Maybe a) where type forall a b. T1 (Maybe a) b = b instance C2 (Maybe a) where type forall b. T2 (Maybe a) b = b }}} But ought it to? There is something funny happening in the `C1` instance: it's explicitly quantifying `a`, despite the fact that it had previously been quantified by the class head! Moreover, it appears that you can safely drop the `a` in the explicit `forall`, as the `C2 (Maybe a)` instance witnesses. What does the documentation have to say on this topic? This is all I could find:
When an explicit `forall` is present, all //type// variables mentioned must be bound by the `forall`.
I couldn't find anything on the interaction between this feature and associated type families. We should: 1. Decide which of the two programs above should be accepted, and 2. Update the documentation to reflect this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15828 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15828: Type family equation foralls allow strange re-quantification of class-bound type variables -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.7 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * cc: mayac (added) Comment: I vote strongly for `C2`. `C1` should be rejected because the local `a` shadows the class-bound `a`, and so the associated type family equation doesn't match its template. You forgot to mention that we need to 3. Fix the implementation. @mayac, do you want to see this (and any other oddities that pop up) through? Or would you prefer that others (perhaps me) fix any problems that arise? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15828#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15828: Type family equation foralls allow strange re-quantification of class-bound type variables -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.7 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by mayac): I also agree `C1` should be rejected, though I'm quite baffled by why that is currently not the case. It appears that the two `a`s in the `C1` example truly do have the same name post-`GhcRn`. Shouldn't `bindLHsTyVarBndrs` be coming up with a fresh name for each explicitly quantified type variable anyway? I don't think I understand enough about the way GHC comes up with new names to see where this goes wrong... In response to @goldfire, I would be happy to address these things as they come up! Of course, if someone finds a fix faster than I do they should feel free to go ahead with the change. In this case, I would need some guidance as I expressed above. As for the documentation, how about the following:
When an explicit `forall` is present, all ''type'' variables mentioned which are not already in scope must be bound by the `forall`.
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15828#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15828: Type family equation foralls allow strange re-quantification of class-bound type variables -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.7 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Shamefully, the answer is not to pass the `mb_cls` to the call to `bindLHsTyVarBndrs` in `rnFamInstEqn` -- always pass `Nothing`. If an associated class is passed in, then `bindLHsTyVarBndrs` uses the in-scope class variables, which is not what's wanted here. Really, only `bindHsQTyVars` should pass a non-`Nothing` in this parameter. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15828#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15828: Type family equation foralls allow strange re-quantification of class-bound type variables -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.7 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5283 Wiki Page: | -------------------------------------+------------------------------------- Changes (by mayac): * differential: => Phab:D5283 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15828#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15828: Type family equation foralls allow strange re-quantification of class-bound type variables -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.7 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5283 Wiki Page: | -------------------------------------+------------------------------------- Comment (by mayac): @goldfire do you think it would be worth including in this fix a comment to the type signature of `bindLHsTyVarBndrs` mentioning that the `mb_cls` argument should usually be `Nothing`? For example: {{{ bindLHsTyVarBndrs :: HsDocContext -> Maybe SDoc -- Just d => check for unused tvs -- d is a phrase like "in the type ..." -> Maybe a -- Just _ => an associated type decl + -- (should be Nothing unless in bindHsQTyVars) -> [LHsTyVarBndr GhcPs] -- User-written tyvars -> ([LHsTyVarBndr GhcRn] -> RnM (b, FreeVars)) -> RnM (b, FreeVars) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15828#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15828: Type family equation foralls allow strange re-quantification of class-bound type variables -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.7 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5283 Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I've answered comment:5 on Phab:D5283 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15828#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15828: Type family equation foralls allow strange re-quantification of class-bound
type variables
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.7
Resolution: | Keywords: TypeFamilies
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s): Phab:D5283
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ryan Scott
#15828: Type family equation foralls allow strange re-quantification of class-bound type variables -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.7 Resolution: fixed | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | rename/should_fail/T15828 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5283 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * testcase: => rename/should_fail/T15828 * status: new => closed * resolution: => fixed * milestone: => 8.8.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15828#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15828: Type family equation foralls allow strange re-quantification of class-bound type variables -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.7 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | rename/should_fail/T15828 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5283 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: simonpj (added) * status: closed => new * resolution: fixed => Comment: Hm... I might have been a little too hasty in closing this ticket. This patch was undoubtedly an improvement over the status quo, as we now throw a proper error instead of silently accepting the original program. However, the error message leaves something to be desired: {{{ T15828.hs:9:3: error: • Type indexes must match class instance head Expected: T (Maybe a) _ Actual: T (Maybe a) b -- Defined at T15828.hs:9:20 • In the type instance declaration for ‘T’ In the instance declaration for ‘C (Maybe a)’ }}} Why did this fail? It's extremely hard to tell, but it's because the two `a` variables aren't the same! I suspect that we're missing some necessary tidying here. Simon, this behavior appears to be new as of your commit 2257a86daa72db382eb927df12a718669d5491f8 (`Taming the Kind Inference Monster`). In particular, this change looks suspicious: {{{#!diff + pp_expected_ty = pprIfaceType (toIfaceType (mkTyConApp fam_tc expected_args)) + -- Do /not/ tidy, because that will rename all those "_" + -- variables we have put in. And (I think) the intance type + -- is already tidy }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15828#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15828: Type family equation foralls allow strange re-quantification of class-bound type variables -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.7 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | rename/should_fail/T15828 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5283 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
Fix a bug in commit 12eeb9 which permits the following:
What is 12eeb9? {{{ $ git show 12eeb9 fatal: ambiguous argument '12eeb9': unknown revision or path not in the working tree. }}} (In an up to date tree.)
hy did this fail? It's extremely hard to tell, but it's because the two a variables aren't the same!
Quite true. So what would we ''like'' to show here? Once we decide that we can think how to achieve it. (It is perhaps fortunate that there is a dedicated pretty-printer for this particular error.) I'm quite keen on using "_" for the bits that don't matter, but if needs must, instead of printing `(F t1 t2 t3)` with one call, we can make separate calls for `t1`, `t2`, `t3` etc, and that would eliminate the need to fake-up a tyvar "_" which you'll see in the code. Would love to have your help if here if you are willing. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15828#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15828: Type family equation foralls allow strange re-quantification of class-bound type variables -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.7 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | rename/should_fail/T15828 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5283 Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:10 simonpj]:
What is 12eeb9?
Quite true. So what would we ''like'' to show here? Once we decide
It's referring to commit 512eeb9bb9a81e915bfab25ca16bc87c62252064 (the leading "5" was simply dropped by mistake). that we can think how to achieve it. I was quite fond of the way it was printed at the time that I landed the patch: {{{ • Type indexes must match class instance head Expected: T (Maybe a1) <tv> Actual: T (Maybe a) b }}} That is, using tidying to emphasize the difference between the two `a`s. Unfortunately, I didn't notice that your commit had changed this until I `validate`d the whole set of patches I was about to commit, at which point I just accepted the new output and moved on. (Upon further thought, I realized the new output was rather smelly, which is why I reopened this ticket.)
I'm quite keen on using "_" for the bits that don't matter
but if needs must, instead of printing `(F t1 t2 t3)` with one call, we can make separate calls for `t1`, `t2`, `t3` etc, and that would eliminate
Sure. I have no preference as to whether we display other type variables as `_`, `<tv>`, or something else. the need to fake-up a tyvar "_" which you'll see in the code. I'm afraid I have no idea what you are referring to with this sentence. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15828#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15828: Type family equation foralls allow strange re-quantification of class-bound
type variables
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone: 8.8.1
Component: Compiler | Version: 8.7
Resolution: | Keywords: TypeFamilies
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
| rename/should_fail/T15828
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s): Phab:D5283
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones
#15828: Type family equation foralls allow strange re-quantification of class-bound type variables -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.7 Resolution: fixed | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | rename/should_fail/T15828 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5283 Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * resolution: => fixed Comment: OK it now prints it the way you had it. Hooray. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15828#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC