Opened 8 months ago

Last modified 3 months ago

#14873 new bug

The well-kinded type invariant (in TcType)

Reported by: RyanGlScott Owned by:
Priority: highest Milestone: 8.8.1
Component: Compiler (Type checker) Version: 8.5
Keywords: TypeInType Cc: simonpj
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash or panic Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

(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

Change History (16)

comment:1 Changed 8 months ago by RyanGlScott

Cc: simonpj added

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

comment:2 Changed 8 months ago by simonpj

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

comment:3 Changed 8 months ago by Simon Peyton Jones <simonpj@…>

In 3d252037/ghc:

Respect Note [The tcType invariant]

I tried to do this with

    commit 0a12d92a8f65d374f9317af2759af2b46267ad5c
    Author: Simon Peyton Jones <simonpj@microsoft.com>
    Date:   Wed Dec 13 12:53:26 2017 +0000

    Further improvements to well-kinded types

    The typechecker has the invariant that every type should be well-kinded
    as it stands, without zonking.  See Note [The well-kinded type invariant]
    in TcType.

    That invariant was not being upheld, which led to Trac #14174.  I fixed
    part of it, but T14174a showed that there was more.  This patch finishes
    the job.

But I didn't get it quite right as Trac #14873 showed.

This patch fixes the problem; although I am still a bit unhappy.
(See "A worry" in the HsApp case of tc_infer_hs_type.)

comment:4 Changed 8 months ago by simonpj

Owner: set to goldfire

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

comment:5 Changed 6 months ago by RyanGlScott

Keywords: TypeInType added

comment:6 Changed 6 months ago by goldfire

I think we need these invariants:

  1. If ty <- tc_hs_type ... exp_kind, then typeKind ty == exp_kind.
  1. If (ty, ki) <- tc_infer_hs_type ..., then typeKind ty == ki.
  1. If (ty, ki) <- tc_infer_hs_type ..., then zonk ki == ki.
  1. If (ty, ki) <- tcTyVar ..., then typeKind ty == ki.
  1. 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?

comment:7 Changed 5 months ago by RyanGlScott

Milestone: 8.6.1

comment:8 Changed 3 months ago by Richard Eisenberg <rae@…>

In cf67e59a/ghc:

Expand and implement Note [The tcType invariant]

Read that note -- it's necessary to make sure that we can
always call typeKind without panicking. As discussed on #14873,
there were more checks and zonking to do, implemented here.
There are no known bugs fixed by this patch, but there are likely
unknown ones.

comment:9 Changed 3 months ago by goldfire

Status: newmerge

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.

comment:10 Changed 3 months ago by simonpj

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.
  1. 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?

Last edited 3 months ago by simonpj (previous) (diff)

comment:11 Changed 3 months ago by simonpj

Summary: GHC HEAD regression (piResultTy)The well-kinded type invariant (in TcType)

comment:12 Changed 3 months ago by Simon Peyton Jones <simonpj@…>

In e24da5e/ghc:

Better Note [The well-kinded type invariant]

c.f. Trac #14873

comment:13 Changed 3 months ago by goldfire

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?

comment:14 Changed 3 months ago by simonpj

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.

comment:15 Changed 3 months ago by bgamari

Owner: goldfire deleted
Status: mergenew

comment:16 Changed 3 months ago by bgamari

Milestone: 8.6.18.8.1
Note: See TracTickets for help on using tickets.