[GHC] #15142: GHC HEAD regression: tcTyVarDetails
#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler | Version: 8.5 (Type checker) | Keywords: TypeInType, | Operating System: Unknown/Multiple TypeFamilies | Architecture: | Type of failure: Compile-time Unknown/Multiple | crash or panic Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This regression prevents the `generic-lens` library from building. Here is a minimized test case: {{{#!hs {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind class ListTuple (tuple :: Type) (as :: [(k, Type)]) where type ListToTuple as :: Type }}} On GHC 8.4.2, this compiles, but on GHC HEAD, it panics: {{{ $ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs[1 of 1] Compiling Bug ( Bug.hs, Bug.o ) ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.5.20180511 for x86_64-unknown-linux): tcTyVarDetails co_aWx :: (k_aWt[tau:2] :: *) ~# (* :: *) Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable pprPanic, called at compiler/basicTypes/Var.hs:497:22 in ghc:Var }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: goldfire (added) Comment: This was introduced in commit faec8d358985e5d0bf363bd96f23fe76c9e281f7 (`Track type variable scope more carefully.`). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Some more observations about this: * If you swap out `TypeInType` for just `DataKinds` and `PolyKinds`, then the program no longer panics, so `TypeInType` appears to be critical in triggering this panic. * If you try and give the parameter to `ListToTuple` an explicit kind signature: {{{#!hs {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind class ListTuple (tuple :: Type) (as :: [(k, Type)]) where type ListToTuple (as :: [(k, Type)]) :: Type }}} Then this will typecheck on GHC 8.4.2, but on HEAD it will give an error message: {{{ $ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:9:29: error: • Expected a type, but ‘k’ has kind ‘k0’ • In the kind ‘[(k, Type)]’ | 9 | type ListToTuple (as :: [(k, Type)]) :: Type | ^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Further observations: * `MultiParamTypeClasses` is also important to triggering this, since this panics: {{{#!hs {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind class C (a :: Type) (b :: k) where type T b }}} But not this: {{{#!hs {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind class C (b :: k) where type T b }}} * The order of arguments to `C`, as well as the exact kind signatures given to them, also appears to be important, as none of the following panics: {{{#!hs {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind class C1 (b :: k) (a :: Type) where type T1 b class C2 b (a :: Type) where type T2 b class C3 b a where type T3 b class C4 (b :: k) a where type T4 b class C5 a (b :: k) where type T5 b class C6 (a :: Type) b where type T6 b class C7 a b where type T7 b }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Comparing the results of `-ddump-tc-trace` on this program: {{{#!hs {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind class C (a :: Type) (b :: k) where type T b }}} On GHC 8.4.2, we have: {{{ kcTyClGroup: initial kinds [r1xu :-> ATcTyCon C :: forall k. * -> k -> Constraint, r1xA :-> ATcTyCon T :: forall k. k -> *] }}} But on GHC HEAD, we have: {{{ kcTyClGroup: initial kinds C :: forall k. * -> k -> Constraint T :: forall (k :: k_a1zm[tau:1]) (co :: k_a1zm[tau:1] GHC.Prim.~# *). (k |> {co_a1zq}) -> * }}} And indeed, `tcTyVarDetails` appears to be panicking on `co`. But I haven't the foggiest idea of what it's doing there... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Oh dear, there are lots of thigs wrong here. I looked at {{{ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind class C (a :: Type) (b :: k) where type T b }}} * First, `C` has a CUSK. But does `T`? Well `hsCeclHasCusk` reports True for the class decl, without even looking at `T`. This seems wrong. * `C` has a CUSK, but in `class C (a :: Type) (b :: k)`, I'm not sore how we get to know that `k :: Type`. Yet, without that `C` would not ahve a CUSK. * `getInitialKinds` returns this very bogus kind for `T`: {{{ kcTyClGroup: initial kinds C :: forall k. * -> k -> Constraint T :: forall (k :: k_aWH[tau:1]) (co :: k_aWH[tau:1] GHC.Prim.~# *). (k |> {co_aWL}) -> * }}} * What is that `co` binder? It's created in the mysterious `kcLHsQTyVars` function, which does something very like `quantifyTyVars`, but by steam. It uses `tyCoVarsOfTypeWellScoped`, but neglects to filter out coercion variables; hence the bugos quantification over `co_aWL`. ------------------ I'm reluctant to reach for a quick fix here. It all looks very dodgy to me. The `getInitialKinds` function, which is the bit misbehaving here, should be very simple: * For CUSKs, the idea is that it's a ''complete, user-specified kind'', just like a top-level type signature for a term variable. II expect to do something very akin to `tcHsSigType`: that is, type-check the kind, solve any constraints that arise, and kind-generalise the result. It's made a bit trickier by the fact that instead of a `LHsSigType` like `forall a. a->a` we have some `LHsQTyVars` like `data T (a :: k) (b :: *)`. But it's basically all one kind signature, pretty much the same as `forall (a::k) (b::*). blah` * For non-CUSKs, we can safely simply make `T :: kappa`, without looking at the declaration at all! We can perhaps save ourselves a bit of fruitless unification by seeing that if its `data T (a :: ...) (b :: ...)` then we can make `T :: kappa1 -> kappa2 -> *`. But we don't have to look into those "..." parts; that's going to happen later. No `solveEqualities` for non-CUSKs. * Associated types should not be allowed to mess things up! They must be treated as CUSK-ish only if they are in fact complete. Fundamentally, the same rules should apply: every type variable should be annotated. But maybe we can make an exception for variables from the parent class, if the parent class has a CUSK. Eg {{{ class C (a :: *) where type F a (b :: * -> *) :: * }}} Here perhaps we can allow `a` not to be annotated in `F`'s defn because it comes from `C` which itself has a CUSK. The present code does not do this, and it's buggy as this ticket shows. Let's discuss. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Oh dear is right. No time to look right now. Will do so next week. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: | TypeFamilies, CUSKs Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: TypeInType, TypeFamilies => TypeInType, TypeFamilies, CUSKs -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: | TypeFamilies, CUSKs Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * owner: (none) => goldfire -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: | TypeFamilies, CUSKs Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Simon says: when there is a CUSK, quantify over any free kind variables. Example at the term level {{{ f :: forall (a :: Proxy k). Proxy a -> Int }}} Then we infer (notice the `k2`): {{{ f :: forall k2 (k :: k2). forall (a :: Proxy k). Proxy a -> Int }}} So similarly at tke type level if we have this CUSK {{{ data T (a :: Proxy k) :: Proxy a -> Type where ... }}} we should quantify over the kind to get {{{ T :: forall k2 (k :: k2). forall (a :: Proxy k). Proxy a -> Type }}} This would require changing code in the CUSK case of `kcLHsQTyVars`, which currently calls `report_non_cusk_tvs` to complain. Instead, generalise. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
For non-CUSKs, we can safely simply make T :: kappa, without looking at
#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: | TypeFamilies, CUSKs Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): the declaration at all! Actually this is not true, as things stand. This accepted: {{{ data T k (a::k) = MkT (Proxy (T * Int)) (Proxy (T (*->*) Maybe)) }}} But `T` does not have a CUSK, and if we assigned it the mono-kind `kappa`, the recursive definition would be rejected. So currently we are cleverly (and somewhat accidentally) accepting a recursive definition with a partial kind signature. I think we should just reject this definition unless you write a CUSK. Specifying exactly what is and what is not accepted would be ... difficult. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: | TypeFamilies, CUSKs Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): This goes back to the kind inference debate we had when working on #14066. The debate is memorialized [https://ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindInference here], toward the top. Suppose we have {{{#!hs data Proxy (k :: Type) (a :: k) = Proxy -- NB: CUSK }}} Do we accept {{{#!hs type ProxySym k a = Proxy k a data ProxyData k a = MkProxyData (Proxy k a) }}} Related are your thoughts on #14847 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: | TypeFamilies, CUSKs Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Some thoughts have been written up [https://ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindInference#SimplifyinggetI... here]. But there's no real progress on what the right answer is. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: | TypeFamilies, CUSKs Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I have good news and bad news. The bad news is that this still does not typecheck on GHC HEAD. The good news is that it no longer panics! It now gives the following, lovely error message: {{{ $ /opt/ghc/head/bin/ghci Bug.hs GHCi, version 8.7.20180621: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:8:42: error: • Expected a type, but ‘k’ has kind ‘k’ • In the kind ‘[(k, Type)]’ | 8 | class ListTuple (tuple :: Type) (as :: [(k, Type)]) where | ^ }}} So that's... nice, I guess. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: | TypeFamilies, CUSKs Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): As far as I can tell, the only available workaround for this issue is to explicitly quantify `k`, like so: {{{#!hs class ListTuple (tuple :: Type) k (as :: [(k, Type)]) where type ListToTuple as :: Type }}} `generic-lens` may need to employ this hack if this issue hasn't been fixed by 8.6.1's release. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15142: GHC HEAD regression: tcTyVarDetails
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: goldfire
Type: bug | Status: new
Priority: highest | Milestone: 8.6.1
Component: Compiler (Type | Version: 8.5
checker) | Keywords: TypeInType,
Resolution: | TypeFamilies, CUSKs
Operating System: Unknown/Multiple | Architecture:
Type of failure: Compile-time | Unknown/Multiple
crash or panic | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg
#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: merge Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: | TypeFamilies, CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: indexed- crash or panic | types/should_compile/T15142 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => merge * testcase: => indexed-types/should_compile/T15142 Comment: Fixed now. Please merge. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: merge Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: | TypeFamilies, CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: indexed- crash or panic | types/should_compile/T15142 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
In 030211d2/ghc:
Richard, I like this. The code is simpler, `kcLHsQTyVars` has a simpler signature. All good. But you did not respond to these points from comment:5: * First, `C` has a CUSK. But does `T`? Well `hsDeclHasCusk` reports True for the class decl, without even looking at `T`. This seems wrong. What is the CUSK status of `T`? Apparently `famDeclHasCusk` returns True if the enclosing class has a CUSK, but is that right? There's a comment "all un-associated open families have CUSKs" which I don't understand. Ah... I see from [http://downloads.haskell.org/~ghc/master/users- guide/glasgow_exts.html#complete-user-supplied-kind-signatures-and- polymorphic-recursion the manual] that we treat open families as CUSK-ish by defaulting. We should have a Note to explain the rules -- or I suppose a Note that summarises and points clearly to the manual as the reference. But why do we default here? It seems inconsistent with (say) `data T a b = ...`. Is it just an arbitrary choice of convenience? What about `type family F (a :: k1 k2) :: *`? * `C` has a CUSK, but in `class C (a :: Type) (b :: k)`, I'm not sure how we get to know that `k :: Type`. Yet, without that `C` would not have a CUSK. I guess that we are defaulting kind variables to `*`? Well not to `*`, because we might have `class C (a :: k1 k2) where ...` After typing this in I realise that all I'm seeking is a clearer exposition of the CUSK rules. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: merge Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: | TypeFamilies, CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: indexed- crash or panic | types/should_compile/T15142 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): The rules are in the [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts... #complete-user-supplied-kind-signatures-and-polymorphic-recursion manual]. There is also `Note [Complete user-supplied kind signatures]`, but I see now that it's a bit out of date. To avoid duplication, I'll just have the Note point to the manual. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: closed Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: fixed | TypeFamilies, CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: indexed- crash or panic | types/should_compile/T15142 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed Comment: Merged with d0dfc5cc4859a07778bc674eb865811616d4d6c6. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: closed Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: fixed | TypeFamilies, CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: indexed- crash or panic | types/should_compile/T15142 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Richard, I have augmented the Note as below. Do you agree with it? On the last point, we say that this does not have a CUSK (taken from `dependent/should_compile/kind_levels`): {{{ data C :: B a -> * }}} But why not? The lexical-forall rule means that it's equivalent to {{{ data C :: forall a. B a -> * }}} which now does have a CUSK. Either the rule needs more justification, or its over-restrictive. Here's the new Note: {{{ {- Note [CUSKs: complete user-supplied kind signatures] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We kind-check declarations differently if they have a complete, user- supplied kind signature (CUSK). This is because we can safely generalise a CUSKed declaration before checking all of the others, supporting polymorphic recursion. See ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindInference#Proposednewstrategy and #9200 for lots of discussion of how we got here. PRINCIPLE: a type declaration has a CUSK iff we could produce a separate kind signature for it, just like a type signature for a function, looking only at the header of the declaration. Examples: * data T1 (a :: *->*) (b :: *) = .... -- Has CUSK; equivalant to T1 :: (*->*) -> * -> * * data T2 a b = ... -- No CUSK; we do not want to guess T2 :: * -> * -> * -- becuase the full decl might be data T a b = MkT (a b) * data T3 (a :: k -> *) (b :: *) = ... -- CUSK; equivalent to T3 :: (k -> *) -> * -> * -- We lexically generalise over k to get -- T3 :: forall k. (k -> *) -> * -> * -- The generalisation is here is purely lexical, just like -- f3 :: a -> a -- means -- f3 :: forall a. a -> a * data T4 (a :: j k) = ... -- CUSK; equivalent to T4 :: j k -> * -- which we lexically generalise to T4 :: forall j k. j k -> * -- and then, if PolyKinds is on, we further generalise to -- T4 :: forall kk (j :: kk -> *) (k :: kk). j k -> * -- Again this is exactly like what happens as the term level -- when you write -- f4 :: forall a b. a b -> Int NOTE THAT * A CUSK does /not/ mean that everything about the kind signature is fully specified by the user. Look at T4 and f4: we had do do kind inference to figure out the kind-quantification. But in both cases (T4 and f4) that inference is done looking /only/ at the header of T4 (or signature for f4), not at the definition thereof. * The CUSK completely fixes the kind of the type constructor, forever. * The precise rules, for each declaration form, for whethher a declaration has a CUSK are given in the user manual section "Complete user- supplied kind signatures and polymorphic recursion". BUt they simply implement PRINCIPLE above. * Open type families are interesting: type family T5 a b :: * There simply /is/ no accompanying declaration, so that info is all we'll ever get. So we it has a CUSK by definition, and we default any un-fixed kind variables to *. * Associated types are a bit tricker: class C6 a where type family T6 a b :: * op :: a Int -> Int Here C6 does not have a CUSK (in fact we ultimately discover that a :: * -> *). And hence neither does T6, the associated family, because we can't fix its kind until we have settled C6. Another way to say it: unlike a top-level, we /may/ discover more about a's kind from C6's definition. * A data definition with a top-level :: must explicitly bind all kind variables to the right of the ::. See test dependent/should_compile/KindLevels, which requires this case. (Naturally, any kind variable mentioned before the :: should not be bound after it.) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: closed Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: fixed | TypeFamilies, CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: indexed- crash or panic | types/should_compile/T15142 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I agree with everything in that Note. Why have the explicit `forall`? Because perhaps the user wants inference, not CUSKness. By making a decision based on the `forall`, then the user can get what they want. For example: {{{#!hs data T1 :: k1 k2 -> Type where MkT1 :: forall (k1 :: Type -> Type) (k2 :: Type) (x :: k1 k2). T1 x }}} There are two possible meanings for this. Meaning 1 (M1): {{{#!hs T1 :: forall (k1 :: Type -> Type) (k2 :: Type). k1 k2 -> Type MkT1 :: forall (k1 :: Type -> Type) (k2 :: Type) (x :: k1 k2). T1 k1 k2 x }}} Meaning 2 (M2): {{{#!hs T1 :: forall (k :: Type) (k1 :: k -> Type) (k2 :: k). k1 k2 -> Type MkT1 :: forall (k :: Type) (k1 :: k -> Type) (k2 :: k) (x :: k1 k2). (k ~# Type) -> T1 k k1 k2 x }}} In M1, we do not quantify `T1`'s kind further, and the data constructor is not GADT-like. In M2, though, we ''do'' generalize, making `MkT1` a GADT constructor packing an equality. M1 is what happens if `T1` does not have a CUSK. `M2` is what happens when it does. Having CUSKness depend on the presence of the `forall` allows users to choose which of these interpretations to use. We ''could'' absolutely, remove it, but then I don't know how to write `T1` with meaning M1. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: closed Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: fixed | TypeFamilies, CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: indexed- crash or panic | types/should_compile/T15142 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): comment:21 is quite debatable as Richard and I agreed on the phone today. It's easier to understand at the term level. Suppose you write {{{ f :: forall a b. a b -> Int f x = let y :: b; y = undefined in 5 }}} With `-XPolyKinds` the type signature is generalised to {{{ f :: forall k. (a :: k->*) (b :: k). a b -> Int }}} But then the definition of `f` is less polymorphic than that! The use of `y::b` forces `b::*`; but the signature says `b::k`, so the definition is rejected. By omitting a `forall` in the final item of the CUSK comment above, the curren system says "not a CUSK", so inference can do its magic. But we can't currently do that in terms. Except perhaps by making a partial type signature like {{{ f :: forall a b. a b -> _ }}} for which inference takes place. The final bullet in the Note, about data types, amounts to a very ad-hoc way of signaling "don't use a CUSK". Ugh. We decided to leave it as-is for now, because we'll end up revisiting all this when we introduce separate kind signatures for type constructors. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15142: GHC HEAD regression: tcTyVarDetails -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: closed Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: TypeInType, Resolution: fixed | TypeFamilies, CUSKs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: indexed- crash or panic | types/should_compile/T15142 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I fully agree with comment:22, including the "Ugh" and not changing it now. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15142#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC