[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
#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]:
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.
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 <ryan.gl.scott@…>): In [changeset:"a57fa24746421c0e13d0c09b72cbabea3622779f/ghc" a57fa247/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="a57fa24746421c0e13d0c09b72cbabea3622779f" Quantify class variables first in associated families' kinds Summary: Previously, `kcLHsQTyVars` would always quantify class-bound variables invisibly in the kinds of associated types, resulting in #15591. We counteract this by explicitly passing the class-bound variables to `kcLHsQTyVars` and quantifying over the ones that are mentioned in the associated type such that (1) they are specified, and (2) they come before other kind variables. See `Note [Kind variable ordering for associated types]`. Test Plan: make test TEST=T15591 Reviewers: goldfire, simonpj, bgamari Reviewed By: simonpj Subscribers: rwbarton, carter GHC Trac Issues: #15591 Differential Revision: https://phabricator.haskell.org/D5159 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15591#comment:12> 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: | -------------------------------------+------------------------------------- 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 <rae@…>): In [changeset:"5e45ad10ffca1ad175b10f6ef3327e1ed8ba25f3/ghc" 5e45ad10/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="5e45ad10ffca1ad175b10f6ef3327e1ed8ba25f3" Finish fix for #14880. The real change that fixes the ticket is described in Note [Naughty quantification candidates] in TcMType. Fixing this required reworking candidateQTyVarsOfType, the function that extracts free variables as candidates for quantification. One consequence is that we now must be more careful when quantifying: any skolems around must be quantified manually, and quantifyTyVars will now only quantify over metavariables. This makes good sense, as skolems are generally user-written and are listed in the AST. As a bonus, we now have more control over the ordering of such skolems. Along the way, this commit fixes #15711 and refines the fix to #14552 (by accepted a program that was previously rejected, as we can now accept that program by zapping variables to Any). This commit also does a fair amount of rejiggering kind inference of datatypes. Notably, we now can skip the generalization step in kcTyClGroup for types with CUSKs, because we get the kind right the first time. This commit also thus fixes #15743 and #15592, which both concern datatype kind generalisation. (#15591 is also very relevant.) For this aspect of the commit, see Note [Required, Specified, and Inferred in types] in TcTyClsDecls. Test cases: dependent/should_fail/T14880{,-2}, dependent/should_fail/T15743[cd] dependent/should_compile/T15743{,e} ghci/scripts/T15743b polykinds/T15592 dependent/should_fail/T15591[bc] ghci/scripts/T15591 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15591#comment:14> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC