Opened 6 years ago

Closed 6 years ago

Last modified 4 years ago

#8566 closed bug (fixed)

Given kind equalities are discarded

Reported by: dreixel Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.7
Keywords: Cc:
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:

Description

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]

Attachments (1)

Bug.hs (615 bytes) - added by dreixel 6 years ago.

Download all attachments as: .zip

Change History (22)

Changed 6 years ago by dreixel

Attachment: Bug.hs added

comment:1 Changed 6 years ago by Simon Peyton Jones <simonpj@…>

In 755823126f4f58b74f2bb783dc683197273f3474/ghc:

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

comment:2 Changed 6 years ago by Simon Peyton Jones <simonpj@…>

comment:3 Changed 6 years ago by simonpj

Resolution: fixed
Status: newclosed

Thank you! This was a real, and long-standing bug. Fixed.

Simon

comment:4 Changed 6 years ago by simonpj

Test Case: polykinds/T8566

comment:5 Changed 6 years ago 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?...

comment:6 Changed 6 years ago 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.

comment:7 Changed 6 years ago 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.

comment:8 Changed 6 years ago by simonpj

Resolution: fixed
Status: closednew
Summary: Panic with kindFunResultGiven kind equalities are discarded

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

Last edited 6 years ago by simonpj (previous) (diff)

comment:9 Changed 6 years ago 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.

comment:10 Changed 6 years ago 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

comment:11 Changed 6 years ago 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.

comment:12 Changed 6 years ago 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

comment:13 Changed 6 years ago 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)?

comment:14 Changed 6 years ago 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

comment:15 Changed 6 years ago 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.

comment:16 Changed 6 years ago by simonpj

Test Case: polykinds/T8566polykinds/T8566, T8566a

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

comment:17 Changed 6 years ago by goldfire

Resolution: fixed
Status: newclosed

Closing ticket, in agreement with Simon. (Closing it as "fixed" because the original bug is indeed fixed.)

comment:18 Changed 6 years ago by Simon Peyton Jones <simonpj@…>

In 45d825bb8ba659696788aca712b6f5d2b15a05cf/ghc:

Add an expect-broken test for Trac #8566

comment:19 Changed 6 years ago by Simon Peyton Jones <simonpj@…>

In 89d2c048c81020a701ac94d949b4d6f1ced37cfa/ghc:

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!

comment:20 Changed 4 years ago by Richard Eisenberg <eir@…>

In 67465497/ghc:

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.

comment:21 Changed 4 years ago by goldfire

Given kind equalities are no longer discarded. And the "expect broken" test case (polykinds/T8566a) now passes.

Note: See TracTickets for help on using tickets.