[GHC] #16116: Explicit foralls in associated type family equations are oblivious to class-bound variables
#16116: Explicit foralls in associated type family equations are oblivious to class-bound variables -------------------------------------+------------------------------------- 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 rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This doesn't typecheck on GHC HEAD: {{{#!hs {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} module Bug where class C a where type T a b instance C (Maybe a) where type forall b. T (Maybe a) b = Either a b }}} {{{ $ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:9:3: error: The RHS of an associated type declaration mentions out-of-scope variable ‘a’ All such variables must be bound on the LHS | 9 | type forall b. T (Maybe a) b = Either a b | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} But it ought to. `a` isn't out of scope at all—it's bound by the class head `instance C (Maybe a)`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16116 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16116: Explicit foralls in associated type family equations are oblivious to class-bound variables -------------------------------------+------------------------------------- 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 rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): The culprit is [http://git.haskell.org/ghc.git/blob/ae4f1033cfe131fca9416e2993bda081e1f8c152... these lines of code] in `rnFamInstEqn`: {{{#!hs ; let bad_tvs = maybe [] (filter is_bad . snd) mb_cls var_name_set = mkNameSet (map hsLTyVarName bndrs' ++ all_imp_var_names) is_bad cls_tkv = cls_tkv `elemNameSet` rhs_fvs && not (cls_tkv `elemNameSet` var_name_set) ; unless (null bad_tvs) (badAssocRhs bad_tvs) }}} `a` //is// in scope over that type family equation, but it's spuriously rejected by this validity check. This check assumes that if a type family equation has an explicit forall, then every type variable on the RHS must either be: 1. Explicitly bound by the `forall`, or 2. Implicitly bound (e.g., as a kind variable) But the sort of program above presents a third option: 3. It's explicitly bound by the class instance, but not by the family equation's `forall`. Unfortunately, this validity check doesn't take this option into account, as evidenced by the implementation of `var_name_set`. I was able to fix this program (and pass GHC's test suite) by changing `var_name_set` to this: {{{#!diff diff --git a/compiler/rename/RnSource.hs b/compiler/rename/RnSource.hs index c76eb31abc..e42f79bd45 100644 --- a/compiler/rename/RnSource.hs +++ b/compiler/rename/RnSource.hs @@ -772,8 +772,9 @@ rnFamInstEqn doc mb_cls rhs_kvars -- See Note [Renaming associated types] ; let bad_tvs = maybe [] (filter is_bad . snd) mb_cls - var_name_set = mkNameSet (map hsLTyVarName bndrs' - ++ all_imp_var_names) + var_name_set = extendNameSetList pat_fvs $ + map hsLTyVarName bndrs' ++ + all_imp_var_names is_bad cls_tkv = cls_tkv `elemNameSet` rhs_fvs && not (cls_tkv `elemNameSet` var_name_set) ; unless (null bad_tvs) (badAssocRhs bad_tvs) }}} I'm not sure if this is the correct approach, however. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16116#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16116: Explicit foralls in associated type family equations are oblivious to class-bound variables -------------------------------------+------------------------------------- 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 rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): @mayac may better remember these details than I. I tend to agree that the original program should be accepted, but perhaps there was a reason not to. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16116#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16116: Explicit foralls in associated type family equations are oblivious to class-bound variables -------------------------------------+------------------------------------- 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 rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Actually this check -- that variables on the RHS are bound on the LHS -- is performed by `TcValidity.checkFamPatBinders`. So I think it can simply be deleted here. It's hard to do correctly because of the implicit kind binders etc. Can you try simply deleting it? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16116#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16116: Explicit foralls in associated type family equations are oblivious to class-bound variables -------------------------------------+------------------------------------- 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 rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): That's a good point. I think that check is a relic from commit 171101beca39befde191baff5027c417bcc709ee, which made an attempt to reject programs like this one: {{{#!hs instance C ('KProxy :: KProxy o) where type F 'KProxy = NatTr (Proxy :: o -> *) }}} Since `o` isn't //explicitly// bound on the left-hand side. However, we later reversed this policy in commit 0829821a6b886788a3ba6989e57e25a037bb6d05, where it was decided that it was OK to mention type variables on the RHSes of type family instances even if they're implicitly bound (i.e., we should accept `F 'KProxy` above). In light of this, I'd agree that `null bad_tvs` validity check serves no purpose. Removing it does make the program work again, (and validates, aside from some expected error message wibbles in `T5515`) which is an encouraging sign. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16116#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16116: Explicit foralls in associated type family equations are oblivious to class-bound variables -------------------------------------+------------------------------------- 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 rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): We should reject egregious examples like {{{ instance C [a] where type F Int = b }}} I hope we do -- and I hope we have a test that checks whether we do. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16116#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16116: Explicit foralls in associated type family equations are oblivious to class-bound variables -------------------------------------+------------------------------------- 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 rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): That example is rejected with a `Not in scope: type variable ‘b’` error, before and after the patch, since `b` is simply not bound anywhere. A more interesting example is the one from `T5515`: {{{#!hs instance ctx a => Bome ctx where type BArg ctx = a }}} This time, `a` technically //is// in scope over the type family equation. However, it's not bound on the LHS of the equation, so it's rejected. After this patch, the new error message becomes: {{{#!diff diff -uw "indexed-types/should_fail/T5515.run/T5515.stderr.normalised" "indexed-types/should_fail/T5515.run/T5515.comp.stderr.normalised" --- indexed-types/should_fail/T5515.run/T5515.stderr.normalised 2019-01-09 11:08:03.005471816 -0500 +++ indexed-types/should_fail/T5515.run/T5515.comp.stderr.normalised 2019-01-09 11:08:03.005471816 -0500 @@ -1,8 +1,24 @@ -T5515.hs:9:3: - The RHS of an associated type declaration mentions out-of-scope variable ‘a’ - All such variables must be bound on the LHS +T5515.hs:6:16: + Expecting one more argument to ‘ctx’ + Expected a type, but ‘ctx’ has kind ‘* -> Constraint’ + In the first argument of ‘Arg’, namely ‘ctx’ + In the first argument of ‘ctx’, namely ‘(Arg ctx)’ + In the class declaration for ‘Bome’ -T5515.hs:15:3: - The RHS of an associated type declaration mentions out-of-scope variable ‘a’ - All such variables must be bound on the LHS +T5515.hs:14:1: + Type variable ‘a’ is mentioned in the RHS, + but not bound on the LHS of the family instance + In the type instance declaration for ‘Arg’ + In the instance declaration for ‘Some f’ + +T5515.hs:14:10: + Could not deduce (C f a0) + from the context: C f a + bound by an instance declaration: + forall f a. C f a => Some f + at T5515.hs:14:10-24 + The type variable ‘a0’ is ambiguous + In the ambiguity check for an instance declaration + To defer the ambiguity check to use sites, enable AllowAmbiguousTypes + In the instance declaration for ‘Some f’ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16116#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16116: Explicit foralls in associated type family equations are oblivious to class-bound variables -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.7 Resolution: | Keywords: 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: | https://gitlab.haskell.org/ghc/ghc/merge_requests/110 -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => https://gitlab.haskell.org/ghc/ghc/merge_requests/110 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16116#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16116: Explicit foralls in associated type family equations are oblivious to class-bound variables -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.7 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | rename/should_compile/T16116a, | rename/should_fail/T16116b Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/110 -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: patch => closed * testcase: => rename/should_compile/T16116a, rename/should_fail/T16116b * resolution: => fixed * milestone: => 8.8.1 Comment: Landed in https://gitlab.haskell.org/ghc/ghc/commit/e63518f5d6a93be111f9108c0990a1162f.... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16116#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16116: Explicit foralls in associated type family equations are oblivious to
class-bound variables
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: closed
Priority: normal | Milestone: 8.8.1
Component: Compiler | Version: 8.7
Resolution: fixed | Keywords:
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: GHC rejects | Test Case:
valid program | rename/should_compile/T16116a,
| rename/should_fail/T16116b
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/110
-------------------------------------+-------------------------------------
Comment (by Ryan Scott
participants (1)
-
GHC