Opened 4 months ago

Last modified 5 weeks ago

#14873 new bug

GHC HEAD regression (piResultTy)

Reported by: RyanGlScott Owned by: goldfire
Priority: highest Milestone: 8.6.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 (7)

comment:1 Changed 4 months ago by RyanGlScott

Cc: simonpj added

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

comment:2 Changed 4 months ago by simonpj

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

comment:3 Changed 4 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 4 months ago by simonpj

Owner: set to goldfire

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

comment:5 Changed 2 months ago by RyanGlScott

Keywords: TypeInType added

comment:6 Changed 2 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 weeks ago by RyanGlScott

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