[GHC] #8566: Panic with kindFunResult
#8566: Panic with kindFunResult ------------------------------------+------------------------------------- Reporter: dreixel | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- The following program: {{{ {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} module Bug where data U (s :: *) = forall k. AA k [U s] data I (u :: U *) (r :: [*]) :: * where A :: I (AA t as) r -- fs unused, but needs to be present for the bug class C (u :: U *) (r :: [*]) (fs :: [*]) where c :: I u r -> I u r instance (C (AA (t (I a ps)) as) ps fs) => C (AA t (a ': as)) ps fs where c A = c undefined }}} crashes a fresh copy of GHC HEAD with the following: {{{ ghc-stage2: panic! (the 'impossible' happened) (GHC version 7.7.20131126 for i386-unknown-linux): kindFunResult k1{tv a24f} [ssk] }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8566> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8566: Panic with kindFunResult -------------------------------------+------------------------------------ Reporter: dreixel | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"755823126f4f58b74f2bb783dc683197273f3474/ghc"]: {{{ #!CommitTicketReference repository="ghc" revision="755823126f4f58b74f2bb783dc683197273f3474" Do not generate given kind-equalities (fix Trac #8566) This is a long-standing bug. We were generating a Given equality between kind variables, and (at least until we support kind coercions) we can't do that. The fix is to drop such Given equalities entirely. That may mean we can't prove some things, but that's fair enough -- the current proof language can't express such proofs. See Note [Do not create Given kind equalities] in TcSMonad }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8566#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8566: Panic with kindFunResult -------------------------------------+------------------------------------ Reporter: dreixel | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"a6e35a07d6d48ce782c5473c03cc09da996e1986/testsuite"]: {{{ #!CommitTicketReference repository="testsuite" revision="a6e35a07d6d48ce782c5473c03cc09da996e1986" Test Trac #8566 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8566#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8566: Panic with kindFunResult -------------------------------------+------------------------------------ Reporter: dreixel | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by simonpj): * status: new => closed * resolution: => fixed Comment: Thank you! This was a real, and long-standing bug. Fixed. Simon -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8566#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8566: Panic with kindFunResult -------------------------------------+------------------------------------ Reporter: dreixel | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: polykinds/T8566 | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by simonpj): * testcase: => polykinds/T8566 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8566#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8566: Panic with kindFunResult -------------------------------------+------------------------------------ Reporter: dreixel | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: polykinds/T8566 | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by dreixel): I suspect this fix makes the following code fail to compile with HEAD: {{{ {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-} data Field = forall k. APP k [Field] data InField (u :: Field) :: * where A :: { unA :: AppVars t (ExpandField args) } -> InField (APP t args) -- Without the selector, the program compiles -- A :: AppVars t (ExpandField args) -> InField (APP t args) type family ExpandField (args :: [Field]) :: [*] type family AppVars (t :: k) (vs :: [*]) :: * }}} Note that simply removing the selector `unA` fixes the problem. The code compiles with 7.6. Is this a regression, or is it the expected behaviour?... -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8566#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8566: Panic with kindFunResult -------------------------------------+------------------------------------ Reporter: dreixel | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: polykinds/T8566 | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): I would say that `unA` in Pedro's (dreixel's) most recent example is indeed ill-typed -- it's an existential record selector, much like {{{ data Ex where MkEx :: { unEx :: [a] } -> Ex }}} The error message, though, could be improved. With `unEx`, GHC accepts the declaration but then prevents any use of `unEx` in an expression position. I propose that the same be done with `unA`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8566#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8566: Panic with kindFunResult -------------------------------------+------------------------------------ Reporter: dreixel | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: polykinds/T8566 | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by simonpj): I had a look at this. I don't agree with Richard: it should typecheck. This `unT` is well typed, despite the GADT: {{{ type family F (a :: *) :: * data T a where MkT :: F a -> T [a] unT :: T [b] -> F b unT (MkT x) = x }}} Here we see that {{{ MkT :: forall u. forall a. (u ~ [a]) => F a -> T u }}} So the 'a' is existential. But from the pattern match we get a Given constraint `[b] ~ [a]`, and we can decompose that to, in effect, determine the existential via a Given equality `b~a`. However that doesn't work in the poly-kinded case of this ticket because the constraint we get is something like `APP k1 (b:k1) ~ APP k2 (a:k2)`. The trouble is that we don't have kind equalities (yet!), so GHC currently decomposes the Given APP constraint, but then silently discards new Given constraint `k1~k2` (since we don't have kind equalities) and `b~a` (because they have incompatible kinds). See `Note [Do not create Given kind equalities]` in `TcSMonad`. The net result is that we can't prove an equality that we "ought" to be able to prove, giving a confusing error message. I do agree with Richard that (until we get kind equalities) it would be better to treat it like an existential record selector, rather than produce the opaque error message. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8566#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8566: Given kind equalities are discarded -------------------------------------+------------------------------------ Reporter: dreixel | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: polykinds/T8566 | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by simonpj): * status: closed => new * resolution: fixed => Comment: Hmm. It occurs to me that with these GADTs it isn't just record selectors that are going to bad on us. Consider {{{ -- Proxy :: forall k. k -> * data T a where MkT :: Proxy b -> T (Proxy b) }}} So the real type of `MkT` is (putting in the kinds) {{{ MkT :: forall u. forall k, b:k. (u ~ Proxy k b) => Proxy k b -> T u }}} Now that `k` is existential. So pattern-matching is going to be problematic. For example, if we write {{{ f :: forall kc, c:kc. T (Proxy kc c) -> Proxy kc c f (MkT x) = x }}} we'll get a Given equality `Proxy kc c ~ Proxy k b`, where the 'k' and 'b' are existentially bound; since we can't make use of such Given equalities, we'll get obscure failures. I rather think that we should '''reject any type signature (including GADT ones) with an equality constraint that mentions a kind variable'''. That would be more restrictive, but it is at least clear. How bad would that be? Simon -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8566#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8566: Given kind equalities are discarded -------------------------------------+------------------------------------ Reporter: dreixel | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: polykinds/T8566 | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): I think that would be bad. For example, take the singleton for lists: {{{ data instance Sing (xs :: [k]) where SNil :: Sing '[] SCons :: Sing h -> Sing t -> Sing (h ': t) }}} The constructors expand to {{{ SNil :: forall (k :: BOX) (xs :: [k]). (xs ~ '[] k) => Sing [k] xs SCons :: forall (k :: BOX) (xs :: [k]). forall (h :: k) (t :: [k]). (xs ~ ((':) k h t)) => Sing k h -> Sing [k] t -> Sing [k] xs }}} (If you get suspicious of the `[k]` in the return type, it's because I didn't unfold the `data instance` piece of it. With that unfolded, the return type's indices are indeed variables.) These equalities mention kind variables, and yet I would be quite sad without them. Or did I miss something here? PS: I take back my claim about `k` being existential and `unA` being ill- typed. Simon is right. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8566#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8566: Given kind equalities are discarded -------------------------------------+------------------------------------ Reporter: dreixel | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: polykinds/T8566 | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by simonpj): Aha. But there is a real difference between the two: {{{ MkT :: forall (u:*). forall (k:BOX), (b:k). (u ~ Proxy k b) => Proxy k b -> T u SNil :: forall (k:BOX) (xs:[k]). (xs ~ '[] k) => Sing22 k xs }}} (I've used `Sing22` for the data type for `Sing (xs:[k])`.) In `SNil` the `k` is univerally quantified over the whole thing. In `MkT` the `k` is existentially quantified, ''and'' involved in an equality constraint. So I rephrase my proposal: '''reject any data constructor with an existentially quantified kind variable that is mentioned in an equality constraint'''. Of course "mentioned in an equality constraint" is itself not too obvious (think superclasses and constraint kinds). But is the direction of travel right? Simon -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8566#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8566: Given kind equalities are discarded -------------------------------------+------------------------------------ Reporter: dreixel | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: polykinds/T8566 | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): I can't find a case where I want an existentially quantified kind variable in an equality constraint, so I think that proposal is viable. ''But'', I think your comment that "'mentioned in an equality constraint' is not obvious" is an understatement. What if a context uses an open type family? Then, we can't know whether or not the type family will expand out to an equality constraint. We could forbid those, too, I suppose, but I don't like where this is going. I might prefer emitting a (suppressable) warning in this case, saying that the user is pushing the type system beyond its limits, really, and to expect the unexpected. Or, we could go the other way and allow such declarations only when the user specifies `-XAllowWonkyExistentialKinds` or similar. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8566#comment:11> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8566: Given kind equalities are discarded -------------------------------------+------------------------------------ Reporter: dreixel | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: polykinds/T8566 | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by simonpj): Maybe we could reject any data constructor whose type risks an existential kind equality (eg including the type-function thing you mention). That would be conservative but safe. Maybe with a flag to say "ok, drop the check and I'll deal with any bad error messages I get". Would you like to try that? Simon -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8566#comment:12> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8566: Given kind equalities are discarded -------------------------------------+------------------------------------ Reporter: dreixel | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: polykinds/T8566 | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): I'm fine with your last suggestion, but I wonder if there's a different way: instead of rejecting the constructor, what if the "bad error messages" suggest the nature of the problem? For example, if a type error occurs after dropping an unusable given kind equality, that error message could say what kind equality was dropped and why. (This is somewhat like error messages that warn about ambiguous variables.) I would imagine that the folks who write the weirdly-existential constructors would be able to understand such a message and respond appropriately. Would this be an engineering challenge (that is, remembering the dropped given equality, just for error reporting)? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8566#comment:13> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8566: Given kind equalities are discarded -------------------------------------+------------------------------------ Reporter: dreixel | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: polykinds/T8566 | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by simonpj): That sounds difficult. We can emit a warning when dropping a given kind equality; indeed, my proposal amounts to ensuring that no such warnings would be generated. But to warn only if we drop a kind equality ''that would (later) be needed to make the program type check'' would be a lot harder. I suppose we could keep the kind-equality and complain only if it was used. But being "used" is different to being "needed". Since you want to add full-on kind equalities, we should not over invest in this... let's just do something simple. (Or even nothing.) Simon -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8566#comment:14> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8566: Given kind equalities are discarded -------------------------------------+------------------------------------ Reporter: dreixel | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: polykinds/T8566 | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): I have to say I like your very last proposal best: do nothing. I wouldn't describe the current wonky behavior as wrong, just perhaps seemingly incomplete. If "doing nothing" makes you queasy, I would just put in the warning, though I'm also fine with blocking the constructor definitions as long as there's a way to unblock them. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8566#comment:15> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8566: Given kind equalities are discarded --------------------------------------------+------------------------------ Reporter: dreixel | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: polykinds/T8566, T8566a | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Changes (by simonpj): * testcase: polykinds/T8566 => polykinds/T8566, T8566a Comment: OK fine. Let's do nothing. I'll add a test `polykinds/T8566a` that fails to compile because of the lack of given kind-equalities, and mark it "expect_broken". Simon -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8566#comment:16> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8566: Given kind equalities are discarded --------------------------------------------+------------------------------ Reporter: dreixel | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: polykinds/T8566, T8566a | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Changes (by goldfire): * status: new => closed * resolution: => fixed Comment: Closing ticket, in agreement with Simon. (Closing it as "fixed" because the original bug is indeed fixed.) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8566#comment:17> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8566: Given kind equalities are discarded --------------------------------------------+------------------------------ Reporter: dreixel | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: polykinds/T8566, T8566a | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"45d825bb8ba659696788aca712b6f5d2b15a05cf/ghc"]: {{{ #!CommitTicketReference repository="ghc" revision="45d825bb8ba659696788aca712b6f5d2b15a05cf" Add an expect-broken test for Trac #8566 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8566#comment:18> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8566: Given kind equalities are discarded --------------------------------------------+------------------------------ Reporter: dreixel | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: polykinds/T8566, T8566a | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"89d2c048c81020a701ac94d949b4d6f1ced37cfa/ghc"]: {{{ #!CommitTicketReference repository="ghc" revision="89d2c048c81020a701ac94d949b4d6f1ced37cfa" Keep kind-inconsistent Given type equalities (fixes Trac #8705) I was too eager when fixing Trac #8566, and dropped too many equalities on the floor, thereby causing Trac #8705. The fix is easy: delete code. Lots of new comments! }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8566#comment:19> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8566: Given kind equalities are discarded ----------------------------------+---------------------------------------- Reporter: dreixel | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: fixed | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Type of failure: None/Unknown | Test Case: polykinds/T8566, T8566a Blocked By: | Blocking: Related Tickets: | ----------------------------------+---------------------------------------- Comment (by Richard Eisenberg <eir@…>): In [changeset:"6746549772c5cc0ac66c0fce562f297f4d4b80a2/ghc" 67465497/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="6746549772c5cc0ac66c0fce562f297f4d4b80a2" Add kind equalities to GHC. This implements the ideas originally put forward in "System FC with Explicit Kind Equality" (ICFP'13). There are several noteworthy changes with this patch: * We now have casts in types. These change the kind of a type. See new constructor `CastTy`. * All types and all constructors can be promoted. This includes GADT constructors. GADT pattern matches take place in type family equations. In Core, types can now be applied to coercions via the `CoercionTy` constructor. * Coercions can now be heterogeneous, relating types of different kinds. A coercion proving `t1 :: k1 ~ t2 :: k2` proves both that `t1` and `t2` are the same and also that `k1` and `k2` are the same. * The `Coercion` type has been significantly enhanced. The documentation in `docs/core-spec/core-spec.pdf` reflects the new reality. * The type of `*` is now `*`. No more `BOX`. * Users can write explicit kind variables in their code, anywhere they can write type variables. For backward compatibility, automatic inference of kind-variable binding is still permitted. * The new extension `TypeInType` turns on the new user-facing features. * Type families and synonyms are now promoted to kinds. This causes trouble with parsing `*`, leading to the somewhat awkward new `HsAppsTy` constructor for `HsType`. This is dispatched with in the renamer, where the kind `*` can be told apart from a type-level multiplication operator. Without `-XTypeInType` the old behavior persists. With `-XTypeInType`, you need to import `Data.Kind` to get `*`, also known as `Type`. * The kind-checking algorithms in TcHsType have been significantly rewritten to allow for enhanced kinds. * The new features are still quite experimental and may be in flux. * TODO: Several open tickets: #11195, #11196, #11197, #11198, #11203. * TODO: Update user manual. Tickets addressed: #9017, #9173, #7961, #10524, #8566, #11142. Updates Haddock submodule. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8566#comment:20> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8566: Given kind equalities are discarded -------------------------------------+------------------------------------- Reporter: dreixel | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | polykinds/T8566, T8566a Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Given kind equalities are no longer discarded. And the "expect broken" test case (polykinds/T8566a) now passes. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8566#comment:21> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC