[GHC] #15591: Inconsistent kind variable binder visibility between associated and non-associated type families
#15591: Inconsistent kind variable binder visibility between associated and non- associated type families -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Keywords: | Operating System: Unknown/Multiple TypeApplications, TypeFamilies | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider the following program and GHCi session which uses it: {{{#!hs {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} module Foo where import Data.Kind type family T1 (x :: f (a :: Type)) class C (a :: Type) where type T2 (x :: f a) }}} {{{ $ ghc2/inplace/bin/ghc-stage2 --interactive Foo.hs -fprint-explicit- foralls GHCi, version 8.7.20180831: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Foo ( Foo.hs, interpreted ) Ok, one module loaded. λ> :kind T1 T1 :: forall (f :: * -> *) a. f a -> * λ> :kind T2 T2 :: forall {a} (f :: * -> *). f a -> * }}} Something is strange about the visibility of `a` in the kinds of `T1` and `T2`. In `T1`, it's visible, but in `T2`, it's not! I would expect them to both be visible, since they were both mentioned by name in each type family's definition. This isn't of much importance at the moment, but it will be once visible kind application lands, as this bug will prevent anyone from instantiating the `a` in `T2` using a kind application. I indicated 8.5 as the version for this ticket since this behavior has changed since GHC 8.4, where you'd get the following: {{{ $ /opt/ghc/8.4.3/bin/ghci Foo.hs -fprint-explicit-foralls GHCi, version 8.4.3: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Foo ( Foo.hs, interpreted ) Ok, one module loaded. λ> :kind T1 T1 :: forall (f :: * -> *) a. f a -> * λ> :kind T2 T2 :: forall (f :: * -> *) a. f a -> * }}} Here, both `a`s are visible. However, it's still wrong in that `a` should be listed before `f` in `T2`'s telescope, since `a` was bound first (in `C`'s class head), before `f`. In that sense, the current behavior is a slight improvement, although we're not fully correct yet. The only difference between `T1` and `T2` is that `T2` is associated with a class, which suggests that there is some difference in code paths between the two that is accounting for this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15591 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15591: Inconsistent kind variable binder visibility between associated and non- associated type families -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | TypeApplications, 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 RyanGlScott): I have somewhat of an idea why this is happening. The [http://git.haskell.org/ghc.git/blob/565ef4cc036905f9f9801c1e775236bb007b026c... bindHsQTyVars] function appears to be partly to blame for this discrepancy. `bindHsQTyVars` (which works over type families, among other things) computes kind variables like so: {{{#!hs implicit_kvs = filter_occs rdr_env bndrs kv_occs }}} Where `filter_occs` is defined as: {{{#!hs filter_occs :: LocalRdrEnv -- In scope -> [Located RdrName] -- Bound here -> [Located RdrName] -- Potential implicit binders -> [Located RdrName] -- Final implicit binders -- Filter out any potential implicit binders that are either -- already in scope, or are explicitly bound here filter_occs rdr_env bndrs occs = filterOut is_in_scope occs where is_in_scope locc@(L _ occ) = isJust (lookupLocalRdrEnv rdr_env occ) || locc `elemRdr` bndrs }}} Note that this filters out any type variable names which appear in `rdr_env`. This environment contains all type variables that have already been bound, which includes any variables that were bound by the class head. Therefore, in our original example, the `a` in `class C (a :: Type)` ends up being filtered out entirely, so by the time we get to typechecking, GHC thinks that `a` is an invisible argument. One idea I had to fix this was to have `filter_occs` also return the class-bound variables so that they could be put at the front of the other kind variables. In other words, this patch: {{{#!diff diff --git a/compiler/rename/RnTypes.hs b/compiler/rename/RnTypes.hs index a78caaf..2163495 100644 --- a/compiler/rename/RnTypes.hs +++ b/compiler/rename/RnTypes.hs @@ -841,7 +841,7 @@ bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside -- Make sure to list the binder kvs before the -- body kvs, as mandated by -- Note [Ordering of implicit variables] - implicit_kvs = filter_occs rdr_env bndrs kv_occs + (cls_bound_nms, implicit_kvs) = filter_occs rdr_env bndrs kv_occs -- Deleting bndrs: See Note [Kind- variable ordering] -- dep_bndrs is the subset of bndrs that are dependent -- i.e. appear in bndr/body_kv_occs @@ -858,13 +858,14 @@ bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside ] ; implicit_kv_nms <- mapM (newTyVarNameRn mb_assoc) implicit_kvs + ; let all_implicit_nms = cls_bound_nms ++ implicit_kv_nms ; bindLocalNamesFV implicit_kv_nms $ bindLHsTyVarBndrs doc mb_in_doc mb_assoc hs_tv_bndrs $ \ rn_bndrs -> do { traceRn "bindHsQTyVars" (ppr hsq_bndrs $$ ppr implicit_kv_nms $$ ppr rn_bndrs) ; dep_bndr_nms <- mapM (lookupLocalOccRn . unLoc) dep_bndrs ; thing_inside (HsQTvs { hsq_ext = HsQTvsRn - { hsq_implicit = implicit_kv_nms + { hsq_implicit = all_implicit_nms , hsq_dependent = mkNameSet dep_bndr_nms } , hsq_explicit = rn_bndrs }) all_bound_on_lhs } } @@ -873,14 +874,25 @@ bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside filter_occs :: LocalRdrEnv -- In scope -> [Located RdrName] -- Bound here -> [Located RdrName] -- Potential implicit binders - -> [Located RdrName] -- Final implicit binders + -> ([Name], [Located RdrName]) + -- (Class binders, final implicit binders) -- Filter out any potential implicit binders that are either -- already in scope, or are explicitly bound here filter_occs rdr_env bndrs occs - = filterOut is_in_scope occs + = partitionWith is_class_bound $ + filterOut is_implicit occs where - is_in_scope locc@(L _ occ) = isJust (lookupLocalRdrEnv rdr_env occ) - || locc `elemRdr` bndrs + is_class_bound :: Located RdrName + -> Either Name (Located RdrName) + -- Left: a class-bound name + -- Right: bound by the type family itself + is_class_bound locc@(L _ occ) = + case lookupLocalRdrEnv rdr_env occ of + Just n -> Left n + Nothing -> Right locc + + is_implicit :: Located RdrName -> Bool + is_implicit locc = locc `elemRdr` bndrs {- Note [bindHsQTyVars examples] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ }}} That fixes the original program, encouragingly enough: {{{ $ inplace/bin/ghc-stage2 --interactive ../Foo.hs -fprint-explicit-foralls GHCi, version 8.7.20180831: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Foo ( ../Foo.hs, interpreted ) Ok, one module loaded. λ> :kind T2 T2 :: forall a (f :: * -> *). f a -> * }}} However, there's a catch. This causes a single test from the test suite to fail: `T14131`. {{{ =====> T14131(normal) 1 of 1 [0, 0, 0] cd "indexed-types/should_compile/T14131.run" && "/home/rgscott/Software/ghc2/inplace/test spaces/ghc-stage2" -c T14131.hs -dcore-lint -dcmm-lint -no-user-package-db -rtsopts -fno-warn- missed-specialisations -fshow-warning-groups -fdiagnostics-color=never -fno-diagnostics-show-caret -dno-debug-output Compile failed (exit code 1) errors were: T14131.hs:29:3: error: • Type indexes must match class instance head Expected: ZT Actual: ZT Use -fprint-explicit-kinds to see the kind arguments • In the class declaration for ‘Z’ *** unexpected failure for T14131(normal) }}} For reference, here's the full definition of `ZT`: {{{#!hs class Z k where type ZT :: Maybe k type ZT = (Nothing :: Maybe k) }}} If you do use `-fprint-explicit-kinds`, the results aren't much more informative: {{{ [1 of 1] Compiling T14131 ( tests/indexed- types/should_compile/T14131.hs, interpreted ) tests/indexed-types/should_compile/T14131.hs:29:3: error: • Type indexes must match class instance head Expected: ZT k Actual: ZT k • In the class declaration for ‘Z’ | 29 | type ZT = (Nothing :: Maybe k) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} I'm still not sure what's going on here—more investigation is required. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15591#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15591: Inconsistent kind variable binder visibility between associated and non- associated type families -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | TypeApplications, 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 RyanGlScott): If nothing else, `ZT` has shown me that my patch in comment:1 isn't sufficient to fix the underlying issue in the first place. If I comment out the default equation for `ZT`, then `:kind ZT` still gives me `forall {k}. Maybe k`, with or without the patch. Back to the drawing board... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15591#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15591: Inconsistent kind variable binder visibility between associated and non- associated type families -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | TypeApplications, 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 RyanGlScott): Oops, it just hit me why I was getting `forall {k}. Maybe k` for `ZT`'s kind even after the patch in comment:1 — `ZT` doesn't have a CUSK! (See #15592 for more on this point in particular.) If I change the definition to this: {{{#!hs class Z (k :: Type) where type ZT :: Maybe k type ZT = (Nothing :: Maybe k) }}} //Then// I get `forall k. Maybe k` for the kind of `ZT`, as expected, and the default definition is no longer rejected. Yay! But all is not well yet. There remains the mystery of why the CUSK-less version of `ZT` is being rejected after applying the patch in comment:1. One clue is that if I apply the patch in comment:1 (and comment out the default definition for `ZT`), then GHCi gives me the following kind for `Z`: {{{ Z :: forall {k}. k -> Constraint }}} This doesn't seem right, since without the patch, I get the following kind for `Z`: {{{ Z :: * -> Constraint }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15591#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15591: Inconsistent kind variable binder visibility between associated and non- associated type families -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | TypeApplications, 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 simonpj): Let's agree the specification first. In this declaration {{{ class C (a :: Type) where type T2 (x :: f a) }}} Then `a` is `Required` for `C`, but presumably it is only `Specified` for `T2`? And what are the rules for Required/Specified/Inferred for type/class declarations that do not have a CUSK? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15591#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15591: Inconsistent kind variable binder visibility between associated and non- associated type families -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | TypeApplications, 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): For comment:4's `C`, I would expect {{{ C :: Type -> Constraint -- a is required, but it's not mentioned by name in the kind T2 :: forall (a :: Type) (f :: Type -> Type). f a -> Type }}} In `T2`'s kind, I've put `a` first, because it was already in scope. This parallels the fact that class variables are quantified before other variables in polymorphic methods. Both `a` and `f` should be `Specified`, as they are user-written. The various `Type`s in the kind of `T2` arise from the defaulting behavior of open type families (unchanged in this conversation). The specification of `Specified`/`Inferred` is very simple: if the user has written the variable name in the declaration, the variable is `Specified`. If not, it's `Inferred`. As for the patch: I would expect that the solution to this problem would be in the type-checker, not the renamer. As it stands, I'm pretty sure that the renamer identifies the `a` in these associated type definitions with the same unique as the `a` in the class. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15591#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15591: Inconsistent kind variable binder visibility between associated and non- associated type families -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | TypeApplications, 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 simonpj):
The specification of Specified/Inferred is very simple: if the user has written the variable name in the declaration, the variable is Specified. If not, it's Inferred.
Regardless of CUSK or non-CUSK? I think so, but let's say so explicitly. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15591#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15591: Inconsistent kind variable binder visibility between associated and non- associated type families -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | TypeApplications, 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): Regardless of CUSK or non-CUSK. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15591#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15591: Inconsistent kind variable binder visibility between associated and non- associated type families -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | TypeApplications, 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 simonpj):
Regardless of CUSK or non-CUSK.
Good. So one action is to add that to the user manual. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15591#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
As for the patch: I would expect that the solution to this problem would be in the type-checker, not the renamer. As it stands, I'm pretty sure
#15591: Inconsistent kind variable binder visibility between associated and non- associated type families -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | TypeApplications, 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 RyanGlScott): Replying to [comment:5 goldfire]: that the renamer identifies the `a` in these associated type definitions with the same unique as the `a` in the class. Well, it does identify the `a` in `T2` to be the same `a` as in `C`. But after it does so, it immediately filters it out! That's problematic, because by the time you reach `kcLHsQTyVars`, the `hsq_implicit` field of the `LHsQTyVars` argument only contains `f`—`a` is no longer within reach. (You can verify this for yourself by compiling this program with `-ddump- tc-trace` and searching for `kcLHsQTyVars: cusk`.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15591#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15591: Inconsistent kind variable binder visibility between associated and non- associated type families -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | TypeApplications, TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #15592 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #15592 * milestone: 8.6.1 => 8.8.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15591#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15591: Inconsistent kind variable binder visibility between associated and non- associated type families -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | TypeApplications, TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #15592 | Differential Rev(s): Phab:D5159 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D5159 Comment: By gum, I think I figured out this one. The trick was to pass the type variables bound by the class directly `kcLHsQTyVars` and to use that to one's advantage. See Phab:D5159. I still haven't figured out how to make the non-CUSK case for `kcLHsQTyVars` work yet (that code confuses the bejeezus out of me), but that's the topic of a separate ticket (#15592) anyway, so I'll leave that for later. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15591#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15591: Inconsistent kind variable binder visibility between associated and non-
associated type families
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: patch
Priority: normal | Milestone: 8.8.1
Component: Compiler | Version: 8.5
Resolution: | Keywords:
| TypeApplications, TypeFamilies
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: #15592 | Differential Rev(s): Phab:D5159
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ryan Scott
#15591: Inconsistent kind variable binder visibility between associated and non- associated type families -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.5 Resolution: fixed | Keywords: | TypeApplications, TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | ghci/scripts/T15591 Blocked By: | Blocking: Related Tickets: #15592 | Differential Rev(s): Phab:D5159 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: patch => closed * testcase: => ghci/scripts/T15591 * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15591#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15591: Inconsistent kind variable binder visibility between associated and non-
associated type families
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: closed
Priority: normal | Milestone: 8.8.1
Component: Compiler | Version: 8.5
Resolution: fixed | Keywords:
| TypeApplications, TypeFamilies
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
| ghci/scripts/T15591
Blocked By: | Blocking:
Related Tickets: #15592 | Differential Rev(s): Phab:D5159
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg
participants (1)
-
GHC