Opened 7 months ago

Last modified 6 months ago

#16188 merge bug

GHC HEAD-only panic (buildKindCoercion)

Reported by: RyanGlScott Owned by: goldfire
Priority: highest Milestone: 8.8.1
Component: Compiler (Type checker) Version: 8.7
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash or panic Test Case: typecheck/should_compile/T16188
Blocked By: Blocking:
Related Tickets: #16204, #16225 Differential Rev(s): https://gitlab.haskell.org/ghc/ghc/merge_requests/207
Wiki Page:

Description

The following program compiles without issue on GHC 8.6.3:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

import Data.Kind (Type)
import Data.Type.Bool (type (&&))

data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: a ~> b) (x :: a) :: b
data family Sing :: forall k. k -> Type

data instance Sing :: Bool -> Type where
  SFalse :: Sing False
  STrue  :: Sing True

(%&&) :: forall (x :: Bool) (y :: Bool).
         Sing x -> Sing y -> Sing (x && y)
SFalse %&& _ = SFalse
STrue  %&& a = a

data RegExp :: Type -> Type where
  App :: RegExp t -> RegExp t -> RegExp t

data instance Sing :: forall t. RegExp t -> Type where
  SApp :: Sing re1 -> Sing re2 -> Sing (App re1 re2)

data ReNotEmptySym0 :: forall t. RegExp t ~> Bool
type instance Apply ReNotEmptySym0 r = ReNotEmpty r

type family ReNotEmpty (r :: RegExp t) :: Bool where
  ReNotEmpty (App re1 re2) = ReNotEmpty re1 && ReNotEmpty re2

sReNotEmpty :: forall t (r :: RegExp t).
               Sing r -> Sing (Apply ReNotEmptySym0 r :: Bool)
sReNotEmpty (SApp sre1 sre2) = sReNotEmpty sre1 %&& sReNotEmpty sre2

blah :: forall (t :: Type) (re :: RegExp t).
        Sing re -> ()
blah (SApp sre1 sre2)
  = case (sReNotEmpty sre1, sReNotEmpty sre2) of
      (STrue, STrue) -> ()

However, it panics on GHC HEAD:

$ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs 
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.7.20190114 for x86_64-unknown-linux):
        buildKindCoercion
  Any
  ReNotEmpty re2_a1hm
  Bool
  t_a1hg
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
        pprPanic, called at compiler/types/Coercion.hs:2427:9 in ghc:Coercion

Change History (9)

comment:1 Changed 7 months ago by RyanGlScott

Here's what you get when you compile the program with -dcore-lint:

$ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs -dcore-lint
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Desugar (before optimization) ***
<no location info>: warning:
    [RHS of ds_d1ur :: (Sing Any, Sing (ReNotEmpty re2_a1hm))]
    The type of this binder doesn't match the type of its RHS: ds_d1ur
    Binder's type: (Sing Any, Sing (ReNotEmpty re2_a1hm))
    Rhs type: (Sing (Apply ReNotEmptySym0 re1_a1hl),
               Sing (ReNotEmpty re2_a1hm))
*** Offending Program ***

<elided>

blah :: forall t (re :: RegExp t). Sing re -> ()
[LclIdX]
blah
  = \ (@ t_a1hg)
      (@ (re_a1hh :: RegExp t_a1hg))
      (ds_d1uq :: Sing re_a1hh) ->
      let {
        ds_d1vi :: R:SingRegExp t_a1hg re_a1hh
        [LclId]
        ds_d1vi
          = ds_d1uq
            `cast` (D:R:SingRegExp0[0] <t_a1hg>_N <re_a1hh>_N
                    :: Sing re_a1hh ~R# R:SingRegExp t_a1hg re_a1hh) } in
      case ds_d1vi of wild_00
      { SApp @ re1_a1hl @ re2_a1hm co_a1hn sre1_aXI sre2_aXJ ->
      let {
        ds_d1ur :: (Sing Any, Sing (ReNotEmpty re2_a1hm))
        [LclId]
        ds_d1ur
          = (sReNotEmpty @ t_a1hg @ re1_a1hl sre1_aXI,
             (sReNotEmpty @ t_a1hg @ re2_a1hm sre2_aXJ)
             `cast` (Sub (Sym (Sing
                                 <Bool>_N
                                 (Sym (D:R:ApplyRegExpBoolReNotEmptySym0r[0]
                                           <t_a1hg>_N <re2_a1hm>_N)))_N)
                     :: Sing (Apply ReNotEmptySym0 re2_a1hm)
                        ~R# Sing (ReNotEmpty re2_a1hm))) } in
      let {
        fail_d1v2 :: Void# -> ()
        [LclId]
        fail_d1v2
          = \ (ds_d1v3 [OS=OneShot] :: Void#) ->
              patError @ 'LiftedRep @ () "Bug.hs:(47,5)-(48,26)|case"# } in
      case ds_d1ur of wild_00 { (ds_d1uY, ds_d1uZ) ->
      let {
        ds_d1v0 :: R:SingBool Any
        [LclId]
        ds_d1v0
          = ds_d1uY
            `cast` (D:R:SingBool0[0] <Any>_N
                    :: Sing Any ~R# R:SingBool Any) } in
      case ds_d1v0 of wild_00 {
        __DEFAULT -> fail_d1v2 void#;
        STrue co_a1hA ->
          let {
            ds_d1v1 :: R:SingBool Any
            [LclId]
            ds_d1v1
              = ds_d1uZ
                `cast` (D:R:SingBool0[0] <Any>_N
                        :: Sing Any ~R# R:SingBool Any) } in
          case ds_d1v1 of wild_00 {
            __DEFAULT -> fail_d1v2 void#;
            STrue co_a1hD -> ()
          }
      }
      }
      }

comment:2 Changed 7 months ago by simonpj

Good catch.

The culprit is here

canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
  = case ev of
     ...

     CtWanted { ctev_dest = dest }
        -> do { traceTcS "canTCAppOk" (ppr bndrs $$ ppr (take 20 tc_roles) $$ ppr tys1 $$ ppr tys2)
              ; cos <- zipWith4M unifyWanted new_locs tc_roles tys1 tys2
              ; setWantedEq dest (mkTyConAppCo role tc cos) }
     ...

  where
    loc        = ctEvLoc ev
    role       = eqRelRole eq_rel
    tc_roles   = tyConRolesX role tc

      -- the following makes a better distinction between "kind" and "type"
      -- in error messages
    bndrs      = tyConBinders tc
    is_kinds   = map isNamedTyConBinder bndrs
    is_viss    = map isVisibleTyConBinder bndrs

    kind_xforms = map (\is_kind -> if is_kind then toKindLoc else id) is_kinds
    vis_xforms  = map (\is_vis  -> if is_vis  then id
                                   else flip updateCtLocOrigin toInvisibleOrigin)
                      is_viss

    -- zipWith3 (.) composes its first two arguments and applies it to the third
    new_locs = zipWith3 (.) kind_xforms vis_xforms (repeat loc)

The equality we are solving is somthing like

  [WD] hole{co_a1hC} {0}:: (Sing
                              @Bool
                              (Apply
                                 @(RegExp t_a1hn[sk:1])
                                 @Bool
                                 (ReNotEmptySym0 @t_a1hn[sk:1])
                                 re1_a1hs[ssk:2]) :: *)
                           GHC.Prim.~#
                           (Sing @Bool a_a1hg[tau:2] :: *)

Turns out that for Sing,

  • its tyConBinders is []
  • so bndrs is []
  • so new_locs is []
  • so cos is []

and we make a coercion Refl Sing,ignoring the arguments to Sing!! Utterly bogus.

The silent assumption of this code is that in T ty1 .. tyn then the tyConBinders of T has length at least n. But that's not true for this data family; and in any case it might not be true of `K (*->*->*) Int Bool Char where K :: forall k. * -> k`; the number of of args depends on how you instantiate it.

The only comment on this code is that it makes a "better distinction between kind and type", and I have no clue how it works. Moreover, it looks terribly smelly: there's a zipWith3 followed by a zipWith4M. We can't really have seven things we want to zip!!

Moreover the zipWith3 is zipping two lists both constructed by map; and the arguments of those maps are ... more maps ... over the same thing, namely bndrs. Lots of huff and puff to do very little.

Richard: all this comes from

commit fb752133f45f01b27240d7cc6bce2063a015e51b
Author: Richard Eisenberg <rae@cs.brynmawr.edu>
Date:   Tue Jul 18 14:30:40 2017 -0400

    Track visibility in TypeEqOrigin

Could you possibly fix the bug, perhaps en route cleaning up the code and adding a Note with a concrete example to explain what is going on? Thanks!

It might also be wise to ASSERT that that cos has the same length as tys1 and tys2, which themselves should have the same length.

comment:3 Changed 7 months ago by simonpj

Owner: set to goldfire

comment:4 Changed 7 months ago by RyanGlScott

#16204 is possibly related.

comment:5 Changed 7 months ago by RyanGlScott

It's unclear to me if this is the same issue or not, but in this slightly modified version of the original program:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wincomplete-patterns #-}
module Bug where

import Data.Kind (Type)
import Data.Type.Bool (type (&&))
import Data.Type.Equality ((:~:)(..))

data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: a ~> b) (x :: a) :: b
data family Sing :: forall k. k -> Type

data instance Sing :: Bool -> Type where
  SFalse :: Sing False
  STrue  :: Sing True

(%&&) :: forall (x :: Bool) (y :: Bool).
         Sing x -> Sing y -> Sing (x && y)
SFalse %&& _ = SFalse
STrue  %&& a = a

data RegExp :: Type -> Type where
  App :: RegExp t -> RegExp t -> RegExp t

data instance Sing :: forall t. RegExp t -> Type where
  SApp :: Sing re1 -> Sing re2 -> Sing (App re1 re2)

data ReNotEmptySym0 :: forall t. RegExp t ~> Bool
type instance Apply ReNotEmptySym0 r = ReNotEmpty r

type family ReNotEmpty (r :: RegExp t) :: Bool where
  ReNotEmpty (App re1 re2) = ReNotEmpty re1 && ReNotEmpty re2

sReNotEmpty :: forall t (r :: RegExp t).
               Sing r -> Sing (Apply ReNotEmptySym0 r :: Bool)
sReNotEmpty (SApp sre1 sre2) = sReNotEmpty sre1 %&& sReNotEmpty sre2

blah :: forall (t :: Type) (re :: RegExp t).
        Sing re -> (ReNotEmpty re :~: True) -> ()
blah (SApp sre1 sre2) Refl
  = case (sReNotEmpty sre1, sReNotEmpty sre2) of
      (STrue, STrue) -> ()

You actually get different pattern-match coverage checker warnings on GHC 8.6 and HEAD! GHC 8.6 compiles with no warnings, whereas on GHC HEAD you get:

$ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:49:5: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: (SFalse, _)
   |
49 |   = case (sReNotEmpty sre1, sReNotEmpty sre2) of
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.7.20190114 for x86_64-unknown-linux):
        buildKindCoercion
  Any
  ReNotEmpty re2_a1mg
  Bool
  t_a1ma
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable
        pprPanic, called at compiler/types/Coercion.hs:2427:9 in ghc:Coercion

It could just be that the types have become so screwed up (due to the explanation in comment:2) that the coverage checker becomes confused, but I thought this was worth pointing out nonetheless.

comment:6 Changed 7 months ago by RyanGlScott

comment:7 Changed 7 months ago by RyanGlScott

Differential Rev(s): https://gitlab.haskell.org/ghc/ghc/merge_requests/207
Status: newpatch

comment:8 Changed 6 months ago by RyanGlScott

Status: patchmerge
Test Case: typecheck/should_compile/T16188

Landed in 4a4ae70f09009c5d32696445a06eacb273f364b5.

Please merge this into 8.8.

comment:9 Changed 6 months ago by Marge Bot <ben+marge-bot@…>

In 4a4ae70/ghc:

Fix #16188

There was an awful lot of zipping going on in
canDecomposableTyConAppOK, and one of the lists being zipped
was too short, causing the result to be too short. Easily
fixed.

Also fixes #16204 and #16225

test case: typecheck/should_compile/T16188
           typecheck/should_compile/T16204[ab]
           typecheck/should_fail/T16204c
           typecheck/should_compile/T16225
Note: See TracTickets for help on using tickets.