The well-kinded type invariant (in TcType)

(Originally noticed here.)

The following program typechecks on GHC 8.2.2 on GHC 8.4.1, but panics on GHC HEAD:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

import Data.Kind (Type)

data family Sing (a :: k)

newtype instance Sing (f :: k1 ~> k2) =
  SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }

data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2

class SingI (a :: k) where
  sing :: Sing a

data ColSym1 :: f a -> a ~> Bool
type instance Apply (ColSym1 x) y = Col x y

class PColumn (f :: Type -> Type) where
  type Col (x :: f a) (y :: a) :: Bool

class SColumn (f :: Type -> Type) where
  sCol :: forall (x :: f a) (y :: a).
    Sing x -> Sing y -> Sing (Col x y :: Bool)

instance (SColumn f, SingI x) => SingI (ColSym1 (x :: f a) :: a ~> Bool) where
  sing = SLambda (sCol (sing @_ @x))

$ /opt/ghc/head/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
  (GHC version 8.5.20180201 for x86_64-unknown-linux):
        piResultTy
  k_aZU[tau:1]
  (a_aW8[sk:1] |> <*>_N)
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable
        pprPanic, called at compiler/types/Type.hs:947:35 in ghc:Type

Trac metadata

Trac field	Value
Version	8.5
Type	Bug
TypeOfFailure	OtherFailure
Priority	highest
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 10

added Tbug Trac import typechecker labels

This regression was introduced in commit 0a12d92a (Further improvements to well-kinded types).

Urk! Patch coming -- but validation is not complete and I have to go home, so probably Monday.

mentioned in commit 3d252037

assigned to @rae

OK done. Richard: could you have a look, to check my work?

mentioned in issue #14904 (closed)

added TypeInType label

I think we need these invariants:

1. If ty <- tc_hs_type ... exp_kind, then typeKind ty == exp_kind.
2. If (ty, ki) <- tc_infer_hs_type ..., then typeKind ty == ki.
3. If (ty, ki) <- tc_infer_hs_type ..., then zonk ki == ki.
4. If (ty, ki) <- tcTyVar ..., then typeKind ty == ki.
5. If (ty, ki) <- tcTyVar ..., then zonk ki == ki.

All of these appear to be true now, except I'm worried about the tcTyVar case for TcTyCons -- I think TcTyCon kinds can have unzonked metavariables, if the TcTyCon comes from the non-CUSK case in kcLHsQTyVars. Do you also think this is possible? If so, we need to zonk the kind and wrap the (knot-tied) type in a reflexive coercion (with mkNakedCastTy) to fix its kind. Do you agree?

changed milestone to %8.6.1

mentioned in commit cf67e59a

This ticket just had some documentation needs to sort out, but along the way, I found places where a few zonks were necessary. I see no reason not to merge.

added 1 deleted label

Richard, I'm beginning to wonder if the pain of Note [The well-kinded type invariant] is worth the gain. It's all very delicate. For example, in the patch above you added some extra zonks; they are unsightly, usually no-ops, potentially inefficient -- and we have no structural guarantee that we've found them all.

Here's a possible alternative

1. Define tcTypeKind :: TcType -> TcM TcKind which zonks, if necessary, on the fly. This would be dead easy to write.
2. Call tcTypeKind instead of typeKind in ... well, in various places. Anywhere in the type checker where un-zonked kinds might be floating about.

For (2) there are two difficulties

• Which calls, exactly, would need to be in the monad?
• Are there any calls that don't have the TcM monad conveniently to hand? For example eqType calls typeKind, so we'd really need a tcEqType variant that calls tcTypeKind.

Advantages: (a) redundant Refls disappear much earlier; this is Good (b) less delicate invariants.

What do you think?

changed title from GHC HEAD regression (piResultTy) to The well-kinded type invariant (in TcType)

mentioned in commit e24da5ed

I've wondered about this, too. If we had TcType separate from Type, then we this would be very easy to find.

I suppose we could smoke it out: put an ASSERT in the typeKind case for TyVarTy that the tyvar isn't a TcTyVar. Do the same with eqType. Then we'd catch (almost) all the cases.

I wonder what the performance implications would be.

(+) We don't have to zonk unnecessarily just to maintain the invariant.

(-) When we do zonk, we don't memorialize this in the type -- only in the kind.

(-) Is monadic code slower than pure code?

Another thing that came up yesterday: there are some calls to eqType where we know for sure the the kinds are the same, so checking the kinds as well is redundant. e.g. the use of eqType in checkExpectedKinds.

removed 1 deleted label

#14873 (closed) merged in 634c07dc.

Leaving open due to ticket:14873#comment:156658.

mentioned in issue #15405 (closed)

changed milestone to %8.8.1

changed milestone to %8.10.1

Bumping milestones of some high and highest priority tickets.

added compiler crash label

Regression test

• polykinds/T14873

added Phighest label

changed milestone to %9.0.1

As it turns out, we've revisited this, in light of #17323, and I think we will have a well-kinded type invariant, in the end. As such, I'm not sure this ticket is serving a purpose. @simonpj?

changed milestone to %9.2.1

Closing since there doesn't seem to be anything to be done here? A regression test has apparently been added already.

closed