Opened 7 weeks ago

Closed 5 weeks ago

#14554 closed bug (fixed)

Core Lint error mixing

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.2.1
Keywords: TypeInType, PolyKinds Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: indexed-types/should_compile/T14554
Blocked By: Blocking:
Related Tickets: #14556 Differential Rev(s):
Wiki Page:

Description

While trying to deeply embed Singletons-style defunctionalization symbol application using the code from System FC with Explicit Kind Equality, I ran into the following -dcore-lint error:

{-# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #-}

import Data.Kind
import Data.Proxy

type a ~> b = (a, b) -> Type

type family (@@) (f::k ~> k') (a::k)::k'

data IdSym0 :: Type ~> Type

type instance IdSym0 @@ a = a

data KIND = X | FNARR KIND KIND

data TY :: KIND -> Type where
  ID    :: TY (FNARR X X)
  FNAPP :: TY (FNARR k k') -> TY k -> TY k'

data TyRep (kind::KIND) :: TY kind -> Type where
  TID    :: TyRep (FNARR X X)  ID
  TFnApp :: TyRep (FNARR k k') f
         -> TyRep k            a
         -> TyRep k'           (FNAPP f a)

type family
  IK (kind::KIND) :: Type where
  IK X            = Type
  IK (FNARR k k') = IK k ~> IK k'

type family
  IT (ty::TY kind) :: IK kind where
  IT ID          = IdSym0
  IT (FNAPP f x) = IT f @@ IT x

zero :: TyRep X a -> IT a
zero = \case
  TFnApp TID a -> undefined 
$ ghci -ignore-dot-ghci -dcore-lint ~/hs/123-bug.hs
GHCi, version 8.3.20171122: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( /home/baldur/hs/123-bug.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.3.20171122 for x86_64-unknown-linux):
	ASSERT failed!
  Bad coercion hole {a2UN}: (IT
                               (a_a1S5 |> Sym (TY (Sym co_a2UC))_N) |> D:R:IK[0])
                            (IT (a_a1S5 |> Sym (TY (Sym co_a2UC))_N) |> D:R:IK[0])
                            nominal
                            <(IT (a_a1S5 |> Sym (TY (Sym co_a2UC))_N) |> D:R:IK[0])>_N
                            IT (a_a1S5 |> Sym (TY (Sym co_a2UC))_N)
                            IT (a_a1S5[ssk:3] |> Sym (TY (Sym co_a2UC))_N)
                            nominal
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1205:22 in ghc:Outputable
        assertPprPanic, called at compiler/typecheck/TcMType.hs:305:105 in ghc:TcMType
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable
        pprPanic, called at compiler/utils/Outputable.hs:1203:5 in ghc:Outputable
        assertPprPanic, called at compiler/typecheck/TcMType.hs:305:105 in ghc:TcMType

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

> 

Change History (4)

comment:1 Changed 6 weeks ago by Iceland_jack

Keywords: TypeInType PolyKinds added

comment:2 Changed 6 weeks ago by RyanGlScott

It's worth noting that what you've posted is a failed ASSERT, not a Core Lint error. Nevertheless, you _do_ experience a Core Lint error if you use a build that doesn't have ASSERTions enabled. Here's what I get with GHC 8.2.2:

[1 of 1] Compiling Main             ( Bug.hs, interpreted )
*** Core Lint errors : in result of Desugar (after optimization) ***
<no location info>: warning:
    [in body of letrec with binders $dIP_a2S7 :: HasCallStack]
    Bad axiom application (check_ki1 D:R:@@TYPETYPEIdSym0a[0]
                                       <IT (a_a1PD |> Sym (TY (Sym (Nth:0 cobox)))_N)>_N
                                     IK 'X
                                     a_a1wo
                                     *)
      D:R:@@TYPETYPEIdSym0a[0]
        <IT (a_a1PD |> Sym (TY (Sym (Nth:0 cobox)))_N)>_N
<no location info>: warning:
    [in body of letrec with binders $dIP_a2S7 :: HasCallStack]
    Bad axiom application (check_ki2 D:R:@@TYPETYPEIdSym0a[0]
                                       <IT (a_a1PD |> Sym (TY (Sym (Nth:0 cobox)))_N)>_N
                                     IK 'X
                                     a_a1wo
                                     *)
      D:R:@@TYPETYPEIdSym0a[0]
        <IT (a_a1PD |> Sym (TY (Sym (Nth:0 cobox)))_N)>_N
<no location info>: warning:
    [in body of letrec with binders $dIP_a2S7 :: HasCallStack]
    Kind application error in
      coercion ‘((@@)
                   (Sym (D:R:IK[0]))
                   (Sym (D:R:IK[0]))
                   (Trans
                        (Sym (Coh <IdSym0>_N
                                  (Trans
                                       (((,) (Sym (D:R:IK[0])) (Sym (D:R:IK[0])))_N ->_N <*>_N)
                                       (Sym (D:R:IK[1] <'X>_N <'X>_N)))))
                        (Sym (Coh (D:R:IT[0]) (D:R:IK[1] <'X>_N <'X>_N))))
                   <IT (a |> (TY (Nth:0 cobox))_N)>_N)_R’
      Function kind = forall k k'. (k ~> k') -> k -> k'
      Arg kinds = [(*, *), (*, *), (IdSym0, (*, *) -> *),
                   (IT (a_a1PD |> (TY (Nth:0 cobox))_N), IK 'X)]
*** Offending Program ***
zero :: forall (a :: TY 'X). TyRep 'X a -> (IT a |> D:R:IK[0])
[LclIdX]
zero
  = \ (@ (a_a1Pz :: TY 'X)) ->
      break<1>()
      \ (ds_d2U1 :: TyRep 'X a_a1Pz) ->
        join {
          fail_d2UH :: Void# -> (IT a_a1Pz |> D:R:IK[0])
          [LclId[JoinId(1)]]
          fail_d2UH _ [Occ=Dead, OS=OneShot]
            = patError
                @ 'LiftedRep
                @ (IT a_a1Pz |> D:R:IK[0])
                "Bug.hs:(37,8)-(38,27)|case"# } in
        case ds_d2U1 of {
          __DEFAULT -> jump fail_d2UH void#;
          TFnApp @ k_a1PB @ f_a1PC @ a_a1PD cobox_a1PE ds_d2UG
                 _ [Occ=Dead] ->
            case ds_d2UG of {
              __DEFAULT -> jump fail_d2UH void#;
              TID cobox_a1PF cobox_a1PG ->
                let {
                  $dIP_a2S7 :: HasCallStack
                  [LclId]
                  $dIP_a2S7
                    = (pushCallStack
                         (unpackCString# "undefined"#,
                          SrcLoc
                            (unpackCString# "main"#)
                            (unpackCString# "Main"#)
                            (unpackCString# "Bug.hs"#)
                            (I# 38#)
                            (I# 19#)
                            (I# 38#)
                            (I# 28#))
                         ((emptyCallStack
                           `cast` (Sym (N:IP[0] <"callStack">_N <CallStack>_N)
                                   :: (CallStack :: *) ~R# ((?callStack::CallStack) :: Constraint))
)
                          `cast` (N:IP[0] <"callStack">_N <CallStack>_N
                                  :: ((?callStack::CallStack) :: Constraint) ~R# (CallStack :: *)))
)
                      `cast` (Sym (N:IP[0] <"callStack">_N <CallStack>_N)
                              :: (CallStack :: *)
                                 ~R#
                                 ((?callStack::CallStack) :: Constraint)) } in
                (break<0>()
                 undefined
                   @ 'LiftedRep
                   @ (IT (a_a1PD |> Sym (TY (Sym (Nth:0 cobox)))_N) |> D:R:IK[0])
                   $dIP_a2S7)
                `cast` (Sym
                          (<(IT
                               (a_a1PD |> Sym (TY (Sym (Nth:0 cobox)))_N) |> D:R:IK[0])>_R |> Sym
                                                                                                D:R
:IK[0])
                        ; Sub
                            (Sym
                               (D:R:@@TYPETYPEIdSym0a[0]
                                  <IT (a_a1PD |> Sym (TY (Sym (Nth:0 cobox)))_N)>_N))
                        ; ((@@)
                             (Sym (D:R:IK[0]))
                             (Sym (D:R:IK[0]))
                             (Trans
                                  (Sym (Coh (Sym <IdSym0>_N)
                                            (Trans
                                                 (((,) (Sym (D:R:IK[0])) (Sym (D:R:IK[0])))_N
                                                  ->_N <*>_N)
                                                 (Sym (D:R:IK[1] <'X>_N <'X>_N)))))
                                  (Sym (Coh (D:R:IT[0]) (D:R:IK[1] <'X>_N <'X>_N))))
                             <IT (a |> (TY (Nth:0 cobox))_N)>_N)_R
                        ; Sub
                            (Sym
                               (D:R:IT[1]
                                  <'X>_N
                                  <'X>_N
                                  <'ID>_N
                                  <(a_a1PD |> Sym (TY (Sym (Nth:0 cobox)))_N)>_N))
                        ; (IT
                             <'X>_N
                             (Trans
                                  ('FNAPP
                                     <'X>_N
                                     (Nth:0 (Sym cobox))
                                     (Trans
                                          (Sym (Coh (Sym (Coh <'ID>_N
                                                              (TY
                                                                 ('FNARR
                                                                    <'X>_N
                                                                    (Nth:1
                                                                         (Nth:0
                                                                              (Sym (Kind
                                                                                        cobox)))))_
N)_N))
                                                    (Sym (Kind cobox))))
                                          (Coh (Sym cobox) (Sym (Kind cobox))))
                                     (Coh <a>_N (TY (Nth:0 cobox))_N))_N
                                  (Sym cobox)))_R
                        ; Sym (<IT a_a1Pz>_R |> D:R:IK[0])
                        :: ((IT
                               (a_a1PD |> Sym (TY (Sym (Nth:0 cobox)))_N) |> D:R:IK[0]) :: *)
                           ~R#
                           ((IT a1_a1Pz |> D:R:IK[0]) :: *))
            }
        }

$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "Main"#)

$krep_a2TJ [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TJ = $WKindRepVar (I# 1#)

$krep_a2TB [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TB = $WKindRepVar (I# 0#)

$krep_a2U0 [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2U0
  = KindRepTyConApp
      $tc(,) (: @ KindRep krep$* (: @ KindRep krep$* ([] @ KindRep)))

$krep_a2TZ [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TZ = KindRepFun $krep_a2U0 krep$*

$krep_a2TK [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TK = $WKindRepVar (I# 2#)

$krep_a2TN [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TN = $WKindRepVar (I# 3#)

$tcIdSym0 :: TyCon
[LclIdX]
$tcIdSym0
  = TyCon
      1961622809926585738##
      3423181666860199358##
      $trModule
      (TrNameS "IdSym0"#)
      0#
      $krep_a2TZ

$tcKIND :: TyCon
[LclIdX]
$tcKIND
  = TyCon
      9515352812269918203##
      11516430088381478906##
      $trModule
      (TrNameS "KIND"#)
      0#
      krep$*

$krep_a2TR [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TR = KindRepTyConApp $tcKIND ([] @ KindRep)

$tc'X :: TyCon
[LclIdX]
$tc'X
  = TyCon
      5225325308912582631##
      14983302646393556978##
      $trModule
      (TrNameS "'X"#)
      0#
      $krep_a2TR

$krep_a2TE [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TE = KindRepTyConApp $tc'X ([] @ KindRep)

$krep_a2TQ [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TQ = KindRepFun $krep_a2TR krep$*

$krep_a2TY [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TY = KindRepFun $krep_a2TR $krep_a2TR

$krep_a2TX [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TX = KindRepFun $krep_a2TR $krep_a2TY

$tc'FNARR :: TyCon
[LclIdX]
$tc'FNARR
  = TyCon
      840343631093516326##
      18087347551297534695##
      $trModule
      (TrNameS "'FNARR"#)
      0#
      $krep_a2TX

$krep_a2TI [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TI
  = KindRepTyConApp
      $tc'FNARR
      (: @ KindRep $krep_a2TJ (: @ KindRep $krep_a2TB ([] @ KindRep)))

$krep_a2TD [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TD
  = KindRepTyConApp
      $tc'FNARR
      (: @ KindRep $krep_a2TE (: @ KindRep $krep_a2TE ([] @ KindRep)))

$tcTY :: TyCon
[LclIdX]
$tcTY
  = TyCon
      11778282896417043628##
      9463294164882319066##
      $trModule
      (TrNameS "TY"#)
      0#
      $krep_a2TQ

$krep_a2TA [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TA
  = KindRepTyConApp $tcTY (: @ KindRep $krep_a2TB ([] @ KindRep))

$krep_a2Tz [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2Tz = KindRepFun $krep_a2TA krep$*

$krep_a2TW [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TW
  = KindRepTyConApp $tcTY (: @ KindRep $krep_a2TJ ([] @ KindRep))

$krep_a2TV [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TV = KindRepFun $krep_a2TW $krep_a2TA

$krep_a2TU [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TU
  = KindRepTyConApp $tcTY (: @ KindRep $krep_a2TI ([] @ KindRep))

$krep_a2TT [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TT = KindRepFun $krep_a2TU $krep_a2TV

$tc'FNAPP :: TyCon
[LclIdX]
$tc'FNAPP
  = TyCon
      7529990373351007495##
      105093863811657267##
      $trModule
      (TrNameS "'FNAPP"#)
      2#
      $krep_a2TT

$krep_a2TP [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TP
  = KindRepTyConApp
      $tc'FNAPP
      (: @ KindRep
         $krep_a2TB
         (: @ KindRep
            $krep_a2TJ
            (: @ KindRep $krep_a2TK (: @ KindRep $krep_a2TN ([] @ KindRep)))))

$krep_a2TS [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TS
  = KindRepTyConApp $tcTY (: @ KindRep $krep_a2TD ([] @ KindRep))

$tc'ID :: TyCon
[LclIdX]
$tc'ID
  = TyCon
      9233083350606244650##
      12129174132981040339##
      $trModule
      (TrNameS "'ID"#)
      0#
      $krep_a2TS

$krep_a2TF [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TF = KindRepTyConApp $tc'ID ([] @ KindRep)

$tcTyRep :: TyCon
[LclIdX]
$tcTyRep
  = TyCon
      5846413146588040822##
      5032305887285000310##
      $trModule
      (TrNameS "TyRep"#)
      1#
      $krep_a2Tz

$krep_a2TO [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TO
  = KindRepTyConApp
      $tcTyRep
      (: @ KindRep $krep_a2TB (: @ KindRep $krep_a2TP ([] @ KindRep)))

$krep_a2TM [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TM
  = KindRepTyConApp
      $tcTyRep
      (: @ KindRep $krep_a2TJ (: @ KindRep $krep_a2TN ([] @ KindRep)))

$krep_a2TL [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TL = KindRepFun $krep_a2TM $krep_a2TO

$krep_a2TH [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TH
  = KindRepTyConApp
      $tcTyRep
      (: @ KindRep $krep_a2TI (: @ KindRep $krep_a2TK ([] @ KindRep)))

$krep_a2TG [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TG = KindRepFun $krep_a2TH $krep_a2TL

$tc'TFnApp :: TyCon
[LclIdX]
$tc'TFnApp
  = TyCon
      8894026854411027209##
      15109781203596368126##
      $trModule
      (TrNameS "'TFnApp"#)
      4#
      $krep_a2TG

$krep_a2TC [InlPrag=[~]] :: KindRep
[LclId]
$krep_a2TC
  = KindRepTyConApp
      $tcTyRep
      (: @ KindRep $krep_a2TD (: @ KindRep $krep_a2TF ([] @ KindRep)))

$tc'TID :: TyCon
[LclIdX]
$tc'TID
  = TyCon
      15519646662091825967##
      1580287496060878##
      $trModule
      (TrNameS "'TID"#)
      0#
      $krep_a2TC

*** End of Offense ***

comment:3 Changed 5 weeks ago by Simon Peyton Jones <simonpj@…>

In b1ea047/ghc:

Fix an outright bug in the unflattener

Trac #14554 showed up an outright bug in the unflattening code in
TcFlatten.  I was filling in a coercion with the wrong coercion (a Syn
in the wrong place).  Result: "Bad coercion hole" assertion failures,
and Core Lint Errors.

Easily fixed, and the code is simpler too.

comment:4 Changed 5 weeks ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: indexed-types/should_compile/T14554
Note: See TracTickets for help on using tickets.