[GHC] #15592: Type families without CUSKs cannot be given visible kind variable binders
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Keywords: | Operating System: Unknown/Multiple TypeApplications, TypeFamilies, | CUSKs | 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: {{{ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} module Foo where import Data.Kind type family T1 (x :: Type) (y :: a) :: Type where {} type family T2 x (y :: a) :: Type where {} }}} {{{ $ 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 a. * -> a -> * λ> :kind T2 T2 :: forall {k} {a}. k -> a -> * }}} Note that `T1` quantifies `a` visibly whereas `T2` does not. I find this somewhat surprising, since both `T1` and `T2` explicitly mention `a` in their respective definitions. The only difference between the two is that `T1` has a CUSK while `T2` does not. This isn't of much importance at the moment, but it will be once visible kind application lands, as this will prevent anyone from instantiating the `a` in `T2` using a kind application. It's unclear to me whether this is intended behavior or not. I suppose there might be an unwritten rule that you can't use visible kind application on anything that doesn't have a CUSK, but if this really is the case, we should be upfront about it. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | TypeApplications, TypeFamilies, | CUSKs 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): Yes, I would expect * In T1 * a is `Specified` * In T2 * k is `Inferred` * a is `Specified` See `Note [TyVarBndrs, TyVarBinders, TyConBinders, and visibility]` in `TyCoRep`. Richard, what do you say? (This will start to bite when we get visible kind application.) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | TypeApplications, TypeFamilies, | CUSKs 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): I agree with comment:1. If a user writes the name of the variable, it is `Specified`. Thus, `a` is specified (in both declarations). `k`, unmentioned, is `Inferred`. But I see some trouble ahead. Consider {{{#!hs data VisProxy k (a :: k) = MkVP class D (a :: Proxy j) (b :: Proxy k) c where meth1 :: forall z. D @j @k a b z => z -> Proxy '(a, b) meth2 :: Proxy k j -> Proxy '(a, b, c) }}} The constraint in `meth1` looks like it's redundantly specifying that `D` should be instantiated at `j` and `k`. I say "redundantly" because `D`, without a CUSK, cannot be polymorphically recursive. However, we discover in `meth2` that `j` actually depends on `k`. So (assuming inference succeeds at all, which I don't wish to debate here), we will get `D :: forall (k :: Type) (j :: k). Proxy j -> Proxy k -> Type -> Constraint`. (The `Type` in the third required argument to `D` comes from `z`'s kind in `meth1`.) Bottom line: any use of visible kind application should be considered to be an instance of polymorphic recursion, and thus should be banned in a mutually recursive group on a CUSK-less type. This is true even if the visible kind application is redundant. Do you agree? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | TypeApplications, TypeFamilies, | CUSKs 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):
Bottom line: any use of visible kind application should be considered to be an instance of polymorphic recursion.
Yes, and we (presumably) have exactly same at the term level {{{ reverse (xs :: [a]) = ...(reverse @a ys).... }}} This is illegal. When type checking `reverse`'s RHS we have `reverse :: alpha` in the envt, and you can't type-apply that to anything. If we had a signature {{{ reverse :: [b] -> [b] reverse (xs :: [a]) = ...(reverse @a ys).... }}} that's fine, because the signature puts `reverse :: forall b. [b] -> [b]` into the envt. This might be a useful example to add to the user-manual documetation for visible type application. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | TypeApplications, TypeFamilies, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #15591 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #15591 * milestone: 8.6.1 => 8.8.1 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | TypeApplications, TypeFamilies, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #15591 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Ah, I now understand why non-CUSKed declarations seem to have totally different behavior with respect to visibility than CUSKed ones: their visibilities are determined in a completely different part of the code! In particular, in `kcTyClGroup` (as opposed to `kcLHsQTyVars`, which was the case for #15591). [http://git.haskell.org/ghc.git/blob/21efbc7599e39ec93b8b13b7d7b84811226e6f6f... This line] is quite relevant: {{{#!hs ; kvs <- kindGeneralize (mkTyConKind tc_binders tc_res_kind) }}} It appears that all kind variables are simply made invisible, which is clearly not what we want. Now we just need to figure out how to bend this code to our will... -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | TypeApplications, TypeFamilies, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: 14880 | Blocking: Related Tickets: #15591 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * blockedby: => 14880 Comment: Hold off on this, please. I've tinkered some in this area en route to #14880 and don't want to duplicate effort. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | TypeApplications, TypeFamilies, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: 14880 | Blocking: Related Tickets: #15591 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Ha ha. I looked at this too. Consider {{{ data T f (a::k1) b = MkT (f a b) }}} Then we should get {{{ T :: forall {k2} k1. (k1 -> k2 -> *) -> k1 -> k2 -> * }}} That is: `k2` is `Inferred` but `k1` is `Specified`. But ''neither'' is among the `tc_binders` of the `TcTyCon` that we make before kind-generalisation! Those `tc_binders` are only the `Required` ones, positionally written by the user. (It took me a while to work this out; we should write it down.) OK so `kindGeneralize` will now generalise over both `k1` and `k1`, in some random order. We must * Mark the `Inferred` ones as `Inferred` and similarly `Specified`. * Put the former before the latter How can we distinguish? Well, the `Specified` ones are among the `tcScopedTyVars` of the `TcTyCon`, but the `Inferred` ones are not. So I did this, in `kcTyClGroup`: {{{ ; kvs <- kindGeneralize (mkTyConKind tc_binders tc_res_kind) ; scoped_tvs' <- zonkTyVarTyVarPairs scoped_tvs ; let (specified_kvs, inferred_kvs) = partition is_specified kvs user_specified_tkvs = mkVarSet (map snd scoped_tvs') is_specified kv = kv `elemVarSet` user_specified_tkvs all_binders = mkNamedTyConBinders Inferred inferred_kvs ++ mkNamedTyConBinders Specified specified_kvs ++ tc_binders }}} This works. I will not commit: over to you Richard. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | TypeApplications, TypeFamilies, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: 14880 | Blocking: Related Tickets: #15591 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): That looks quite sensible and is independent from what I've done. (I was thinking we might have to put these into the `tc_binders`, but that's hard to get right for a non-CUSK.) If what you have works, feel free to commit. It won't get in my way. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | TypeApplications, TypeFamilies, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: 14880 | Blocking: Related Tickets: #15591 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): By a series of strange coincidences, I ended up with almost exactly the same code as in comment:7 while working on this this morning. (Don't worry, I won't work on this any further until the dust has settled on #14880.) There's one thing I haven't worked out, though: how to make this work for associated types (in light of #15591). Consider: {{{#!hs class C a where type T (x :: f a) }}} Ideally, the kind of `T` would be: {{{#!hs T :: forall {k} (a :: k) (f :: k -> Type). f a -> Type }}} Alas, the code in comment:7 is not enough to accomplish this. It will instead give this as the kind for `T`: {{{#!hs T :: forall {k} {a :: k} (f :: k -> Type). f a -> Type }}} Note that `a` is now invisible. Ack. In order to fix this, we'd need to be aware of the fact that `a` is mentioned explicitly in `C` within `kcTyClGroup`. Currently, `kcTyClGroup` doesn't have access to this information, however. Another gotcha is that if you only use the code in comment:7, it'll cause some programs to no longer typecheck. In particular, this program: {{{#!hs class C a where type T (x :: (f :: k -> Type) a) }}} {{{ Bug.hs:8:3: error: • These kind and type variables: (x :: (f :: k -> Type) a) are out of dependency order. Perhaps try this ordering: k (a :: k) (f :: k -> *) (x :: f a) NB: Implicitly declared variables come before others. • In the associated type family declaration for ‘T’ | 8 | type T (x :: (f :: k -> Type) a) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} I'm unclear if this is desirable or not. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | TypeApplications, TypeFamilies, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: 14880 | Blocking: Related Tickets: #15591 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
In order to fix this, we'd need to be aware of the fact that a is mentioned explicitly in C within kcTyClGroup. Currently, kcTyClGroup doesn't have access to this information, however.
Hmm. I wonder if we should simply add `a` to the `tyConScopedTyVars` of `T`? And that info ''is'' available in `kcLHsTQTVars` which builds the `TcTyCon`. Richard? Maybe that'd fix the gotcha too? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | TypeApplications, TypeFamilies, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: 14880 | Blocking: Related Tickets: #15591 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:10 simonpj]:
Hmm. I wonder if we should simply add `a` to the `tyConScopedTyVars` of `T`? And that info ''is'' available in `kcLHsTQTVars` which builds the `TcTyCon`.
I too am a bit confused as to why we don't add `a` (or any kind variables, for that matter) to `tcTyConScopedTyVars` in the non-CUSK case of `kcLHsQTyVars`. The only reasoning I could find for this design choice is [http://git.haskell.org/ghc.git/blob/fc2ff6dd7496a33bf68165b28f37f40b7d647418... this terse comment]: {{{#!hs ; let -- NB: Don't add scoped_kvs to tyConTyVars, because they -- must remain lined up with the binders tc_binders = zipWith mk_tc_binder hs_tvs tc_tvs tycon = mkTcTyCon name (ppr user_tyvars) tc_binders res_kind (mkTyVarNamePairs (scoped_kvs ++ tc_tvs)) flav }}} (Here, they call `tcTyConScopedTyVars` "`tyConTyVars`".) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:11> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | TypeApplications, TypeFamilies, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: 14880 | Blocking: Related Tickets: #15591 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I discovered that this bug fix has a visible effect! Consider this in `GHC.Records`: {{{ -- | Constraint representing the fact that the field @x@ belongs to -- the record type @r@ and has field type @a@. This will be solved -- automatically, but manual instances may be provided as well. class HasField (x :: k) r a | x r -> a where -- | Selector function to extract the field from the record. getField :: r -> a }}} What is the kind of `HasField` and type of `getField`? As of today, GHC says {{{ HasField :: forall {k}. k -> * -> * -> Constraint getField :: forall {k] (x::k) r a. HasField x r a => r -> a }}} But actually, because of the `(x :: k)` in the class decl, the `k` is `Specified`. So the correct kind and type are: {{{ HasField :: forall k. k -> * -> * -> Constraint getField :: forall k (x::k) r a. HasField x r a => r -> a }}} So in a visible type application of `getField` you'd have to write `getField @Symbol @x`. But that is not what Adam intended. We don't want to be forced to write that kind, even in a visible type application. We want `k` to be `Inferred`. I can achieve this for now by changing the decl to {{{ class HasField x r a | x r -> a where getField :: r -> a }}} so removing the `:: k` from the decl. But that is rather subtle. I'm looking forward to explicit kind signatures... but NB: they need to be able to express the `Inferred`/`Specified` distinction. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:12> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | TypeApplications, TypeFamilies, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: 14880 | Blocking: Related Tickets: #15591 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"2f09753f96207c12efd43090f5de55b05aef35d3/ghc" 2f09753f/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="2f09753f96207c12efd43090f5de55b05aef35d3" Distinguish Inferred from Specified tyvars In a declared type we need to distinguish between Inferred and Specified type variables. This was exposed by Trac #15592. See Note [Work out final tyConBinders] in TcTyClsDecls. I had to change the definition of HasField in GHC.Records to class HasField x r a | x r -> a where so as to have an /inferred/ kind argument rather than a specfied one. So HasField :: forall {k}. k -> * -> * -> Constraint }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:13> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | TypeApplications, TypeFamilies, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: 14880 | Blocking: Related Tickets: #15591 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): OK so I've done the first bit. We still need to address comment:9 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:14> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | TypeApplications, TypeFamilies, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: 14880 | Blocking: Related Tickets: #15591 | Differential Rev(s): 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/15592#comment:15> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | TypeApplications, TypeFamilies, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: 14880 | Blocking: Related Tickets: #15591 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): After the commit in comment:15, the program from comment:9: {{{#!hs class C a where type T (x :: (f :: k -> Type) a) }}} Now typechecks again. There doesn't appear to be a test case for this, however. Worth checking in? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:16> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | TypeApplications, TypeFamilies, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: 14880 | Blocking: Related Tickets: #15591 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I thought I did add this, though perhaps to a T15991 test. I'm out of cycles now for a few days, but please add if you can't find it. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:17> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | TypeApplications, TypeFamilies, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: 14880 | Blocking: Related Tickets: #15591 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Ryan Scott <ryan.gl.scott@…>): In [changeset:"42faeb3bf0a167ec4d449f27d8ca37501d96d24d/ghc" 42faeb3/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="42faeb3bf0a167ec4d449f27d8ca37501d96d24d" Add second test case for #15592 This adds a program from https://ghc.haskell.org/trac/ghc/ticket/15592#comment:9 (which briefly refused to typecheck on GHC HEAD) as a test case. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:18> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: fixed | Keywords: | TypeApplications, TypeFamilies, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | polykinds/T15592{,b} Blocked By: 14880 | Blocking: Related Tickets: #15591 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * testcase: => polykinds/T15592{,b} * status: new => closed * resolution: => fixed -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:19> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | TypeApplications, TypeFamilies, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | polykinds/T15592{,b} Blocked By: 14880 | Blocking: Related Tickets: #15591 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: closed => new * resolution: fixed => Comment: Concerning comment:16 we need to be careful We certainly have `C :: forall {k}. k -> Constraint`. So `k` is `Inferred` and `a` is `Required`. Now look at `T`. I think we want {{{ T :: forall k (a::k) (f :: k->Type). f a -> Type }}} That is: `k` must be `Specified` (because the user wrote it); but it must precede the `a` which comes from the class. On the other hand, if `T` didn't mention `k` it'd be `Inferred`. What about this? {{{ class D (a::k) where type S a }}} Here `k` is `Specified` for `D`, but is it `Specified` or `Inferred` for `S`? The notes in `Note [Required, Specified, and Inferred for types]` do not really answer this question. This business of thinking about how the class header affects the Inferred/Specified/Required spec for the associated type is desperately tricky. I still wonder if we should instead look at the type declaration alone. An improvement would be this: * Whether the tyvar is Inferred or Specified is determined by looking at the associated type (alone) * But the order in which the Specified variables appear is affected by the class header. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:20> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | TypeApplications, TypeFamilies, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | polykinds/T15592{,b} Blocked By: 14880 | Blocking: Related Tickets: #15591 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Richard and I talked more about this. We worreid abou {{{ class C a b whre type T (x :: b a) }}} In what order do T's Specified variables show up? We got as far as a detailed proposal for associated types: * Which vars are Specified and which Inferred is determined by type decl alone (Specified = explicitly mentioned in the type decl) • For the Specified variables: * Start with lexical order from type decl * Do a stable partition, moving the ones from the class decl to the front * Use ScopedSort to put them in dependency order. But it all seemed terribly complicated. We ended up thinking that it'd be better to ''ingnore'' the class header, and just do the normal thing: * Start with the lexical order from the type decl * Use ScopedSort This simplifies the spec, and simplifies the code. It is a bit unlike what happens for class methods (where the class variables all show up at the front, but we have no idea how to do make associated types really behave like class methods. Eg {{{ class C a where type F a }}} Then perhaps `F :: forall a -> C a => Type`, which is not ery nice. And it gets worse {{{ class C a b where type F a }}} then perhaps `F :: forall {b}. forall a -> C a b => Type`. Ugh. But if `b` depends on `a` we'd have to put it later in the telescope. So we decided to keep it simple! (This is a small change from the commit in comment:15). -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:21> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | TypeApplications, TypeFamilies, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | polykinds/T15592{,b} Blocked By: 14880 | Blocking: Related Tickets: #15591 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Just to chime in agreement with comment:21. I'm sympathetic to the desire to put class variables first, but it gets ugly quickly. Here's another example: {{{#!hs class C a where type F (x :: (f :: k -> Type) a) }}} Here, `k` is actually a ''class'' variable, even though that's highly non- obvious. So `k` should go in the first clump of variables. But it would be easy to assume that `k`, not mentioned in the class header, goes with the second clump of variables. In the end, I agreed that there are just too many wrinkles in the "class variables come first" design, and went with "infer variable order / visibility locally" instead. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:22> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: | TypeApplications, TypeFamilies, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | polykinds/T15592{,b} Blocked By: 14880 | Blocking: Related Tickets: #15591 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"2257a86daa72db382eb927df12a718669d5491f8/ghc" 2257a86d/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="2257a86daa72db382eb927df12a718669d5491f8" Taming the Kind Inference Monster My original goal was (Trac #15809) to move towards using level numbers as the basis for deciding which type variables to generalise, rather than searching for the free varaibles of the environment. However it has turned into a truly major refactoring of the kind inference engine. Let's deal with the level-numbers part first: * Augment quantifyTyVars to calculate the type variables to quantify using level numbers, and compare the result with the existing approach. That is; no change in behaviour, just a WARNing if the two approaches give different answers. * To do this I had to get the level number right when calling quantifyTyVars, and this entailed a bit of care, especially in the code for kind-checking type declarations. * However, on the way I was able to eliminate or simplify a number of calls to solveEqualities. This work is incomplete: I'm not /using/ level numbers yet. When I subsequently get rid of any remaining WARNings in quantifyTyVars, that the level-number answers differ from the current answers, then I can rip out the current "free vars of the environment" stuff. Anyway, this led me into deep dive into kind inference for type and class declarations, which is an increasingly soggy part of GHC. Richard already did some good work recently in commit 5e45ad10ffca1ad175b10f6ef3327e1ed8ba25f3 Date: Thu Sep 13 09:56:02 2018 +0200 Finish fix for #14880. The real change that fixes the ticket is described in Note [Naughty quantification candidates] in TcMType. but I kept turning over stones. So this patch has ended up with a pretty significant refactoring of that code too. Kind inference for types and classes ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ * Major refactoring in the way we generalise the inferred kind of a TyCon, in kcTyClGroup. Indeed, I made it into a new top-level function, generaliseTcTyCon. Plus a new Note to explain it Note [Inferring kinds for type declarations]. * We decided (Trac #15592) not to treat class type variables specially when dealing with Inferred/Specified/Required for associated types. That simplifies things quite a bit. I also rewrote Note [Required, Specified, and Inferred for types] * Major refactoring of the crucial function kcLHsQTyVars: I split it into kcLHsQTyVars_Cusk and kcLHsQTyVars_NonCusk because the two are really quite different. The CUSK case is almost entirely rewritten, and is much easier because of our new decision not to treat the class variables specially * I moved all the error checks from tcTyClTyVars (which was a bizarre place for it) into generaliseTcTyCon and/or the CUSK case of kcLHsQTyVars. Now tcTyClTyVars is extremely simple. * I got rid of all the all the subtleties in tcImplicitTKBndrs. Indeed now there is no difference between tcImplicitTKBndrs and kcImplicitTKBndrs; there is now a single bindImplicitTKBndrs. Same for kc/tcExplicitTKBndrs. None of them monkey with level numbers, nor build implication constraints. scopeTyVars is gone entirely, as is kcLHsQTyVarBndrs. It's vastly simpler. I found I could get rid of kcLHsQTyVarBndrs entirely, in favour of the bnew bindExplicitTKBndrs. Quantification ~~~~~~~~~~~~~~ * I now deal with the "naughty quantification candidates" of the previous patch in candidateQTyVars, rather than in quantifyTyVars; see Note [Naughty quantification candidates] in TcMType. I also killed off closeOverKindsCQTvs in favour of the same strategy that we use for tyCoVarsOfType: namely, close over kinds at the occurrences. And candidateQTyVars no longer needs a gbl_tvs argument. * Passing the ContextKind, rather than the expected kind itself, to tc_hs_sig_type_and_gen makes it easy to allocate the expected result kind (when we are in inference mode) at the right level. Type families ~~~~~~~~~~~~~~ * I did a major rewrite of the impenetrable tcFamTyPats. The result is vastly more comprehensible. * I got rid of kcDataDefn entirely, quite a big function. * I re-did the way that checkConsistentFamInst works, so that it allows alpha-renaming of invisible arguments. * The interaction of kind signatures and family instances is tricky. Type families: see Note [Apparently-nullary families] Data families: see Note [Result kind signature for a data family instance] and Note [Eta-reduction for data families] * The consistent instantation of an associated type family is tricky. See Note [Checking consistent instantiation] and Note [Matching in the consistent-instantation check] in TcTyClsDecls. It's now checked in TcTyClsDecls because that is when we have the relevant info to hand. * I got tired of the compromises in etaExpandFamInst, so I did the job properly by adding a field cab_eta_tvs to CoAxBranch. See Coercion.etaExpandCoAxBranch. tcInferApps and friends ~~~~~~~~~~~~~~~~~~~~~~~ * I got rid of the mysterious and horrible ClsInstInfo argument to tcInferApps, checkExpectedKindX, and various checkValid functions. It was horrible! * I got rid of [Type] result of tcInferApps. This list was used only in tcFamTyPats, when checking the LHS of a type instance; and if there is a cast in the middle, the list is meaningless. So I made tcInferApps simpler, and moved the complexity (not much) to tcInferApps. Result: tcInferApps is now pretty comprehensible again. * I refactored the many function in TcMType that instantiate skolems. Smaller things * I rejigged the error message in checkValidTelescope; I think it's quite a bit better now. * checkValidType was not rejecting constraints in a kind signature forall (a :: Eq b => blah). blah2 That led to further errors when we then do an ambiguity check. So I make checkValidType reject it more aggressively. * I killed off quantifyConDecl, instead calling kindGeneralize directly. * I fixed an outright bug in tyCoVarsOfImplic, where we were not colleting the tyvar of the kind of the skolems * Renamed ClsInstInfo to AssocInstInfo, and made it into its own data type * Some fiddling around with pretty-printing of family instances which was trickier than I thought. I wanted wildcards to print as plain "_" in user messages, although they each need a unique identity in the CoAxBranch. Some other oddments * Refactoring around the trace messages from reportUnsolved. * A bit of extra tc-tracing in TcHsSyn.commitFlexi This patch fixes a raft of bugs, and includes tests for them. * #14887 * #15740 * #15764 * #15789 * #15804 * #15817 * #15870 * #15874 * #15881 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:23> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: fixed | Keywords: | TypeApplications, TypeFamilies, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | polykinds/T15592, T15592b Blocked By: 14880 | Blocking: Related Tickets: #15591 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * testcase: polykinds/T15592{,b} => polykinds/T15592, T15592b * status: new => closed * resolution: => fixed -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:24> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: fixed | Keywords: | TypeApplications, TypeFamilies, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | polykinds/T15592{b}, | typecheck/should_fail/T15592a Blocked By: 14880 | Blocking: Related Tickets: #15591 | Differential Rev(s): Phab:D5229 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * testcase: polykinds/T15592, T15592b => polykinds/T15592{b}, typecheck/should_fail/T15592a * differential: => Phab:D5229 Comment: A test case for comment:2 was added in [https://gitlab.haskell.org/ghc/ghc/commit/17bd163566153babbf51adaff8397f948a... 17bd163566153babbf51adaff8397f948ae363ca]: {{{ Author: mynguyen <mnguyen1@brynmawr.edu> Date: Tue Dec 18 11:52:26 2018 -0500 Visible kind application Summary: This patch implements visible kind application (GHC Proposal 15/#12045), as well as #15360 and #15362. It also refactors unnamed wildcard handling, and requires that type equations in type families in Template Haskell be written with full type on lhs. PartialTypeSignatures are on and warnings are off automatically with visible kind application, just like in term-level. There are a few remaining issues with this patch, as documented in ticket #16082. Includes a submodule update for Haddock. Test Plan: Tests T12045a/b/c/TH1/TH2, T15362, T15592a Reviewers: simonpj, goldfire, bgamari, alanz, RyanGlScott, Iceland_jack Subscribers: ningning, Iceland_jack, RyanGlScott, int-index, rwbarton, mpickering, carter GHC Trac Issues: `#12045`, `#15362`, `#15592`, `#15788`, `#15793`, `#15795`, `#15797`, `#15799`, `#15801`, `#15807`, `#15816` Differential Revision: https://phabricator.haskell.org/D5229 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:25> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15592: Type families without CUSKs cannot be given visible kind variable binders -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: fixed | Keywords: | TypeApplications, TypeFamilies, | CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | polykinds/T15592{b}, | typecheck/should_fail/T15592a Blocked By: 14880 | Blocking: Related Tickets: #15591 | Differential Rev(s): Phab:D5229 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg <rae@…>): In [changeset:"17bd163566153babbf51adaff8397f948ae363ca/ghc" 17bd1635/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="17bd163566153babbf51adaff8397f948ae363ca" Visible kind application Summary: This patch implements visible kind application (GHC Proposal 15/#12045), as well as #15360 and #15362. It also refactors unnamed wildcard handling, and requires that type equations in type families in Template Haskell be written with full type on lhs. PartialTypeSignatures are on and warnings are off automatically with visible kind application, just like in term-level. There are a few remaining issues with this patch, as documented in ticket #16082. Includes a submodule update for Haddock. Test Plan: Tests T12045a/b/c/TH1/TH2, T15362, T15592a Reviewers: simonpj, goldfire, bgamari, alanz, RyanGlScott, Iceland_jack Subscribers: ningning, Iceland_jack, RyanGlScott, int-index, rwbarton, mpickering, carter GHC Trac Issues: `#12045`, `#15362`, `#15592`, `#15788`, `#15793`, `#15795`, `#15797`, `#15799`, `#15801`, `#15807`, `#15816` Differential Revision: https://phabricator.haskell.org/D5229 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15592#comment:26> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC