[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
#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
#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
#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
#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
#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