Typed hole panic on GHC 8.6 (tcTyVarDetails)

The following program panics on GHC 8.6 and HEAD:

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

import Data.Kind
import Data.Type.Equality
import Data.Void

data family Sing :: forall k. k -> Type

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

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

mkRefl :: n :~: j
mkRefl = Refl

right :: forall (r :: (x :~: y) ~> z).
         Sing r -> ()
right no =
  case mkRefl @x @y of
    Refl -> applySing no _

$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
  (GHC version 8.6.0.20180627 for x86_64-unknown-linux):
        tcTyVarDetails
  co_a1BG :: y_a1Bz[sk:1] ~# x_a1By[sk:1]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
        pprPanic, called at compiler/basicTypes/Var.hs:497:22 in ghc:Var

On GHC 8.4, this simply errors:

$ /opt/ghc/8.4.3/bin/ghc Bug.hs   
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:23:10: error:
    • Couldn't match type ‘n’ with ‘j’
      ‘n’ is a rigid type variable bound by
        the type signature for:
          mkRefl :: forall k1 (n :: k1) (j :: k1). n :~: j
        at Bug.hs:22:1-17
      ‘j’ is a rigid type variable bound by
        the type signature for:
          mkRefl :: forall k1 (n :: k1) (j :: k1). n :~: j
        at Bug.hs:22:1-17
      Expected type: n :~: j
        Actual type: n :~: n
    • In the expression: Refl
      In an equation for ‘mkRefl’: mkRefl = Refl
    • Relevant bindings include
        mkRefl :: n :~: j (bound at Bug.hs:23:1)
   |
23 | mkRefl = Refl
   |          ^^^^

Bug.hs:29:13: error:
    • Couldn't match type ‘Sing (Apply r t0)’ with ‘()’
      Expected type: ()
        Actual type: Sing (Apply r t0)
    • In the expression: applySing no _
      In a case alternative: Refl -> applySing no _
      In the expression: case mkRefl @x @y of { Refl -> applySing no _ }
    • Relevant bindings include
        no :: Sing r (bound at Bug.hs:27:7)
        right :: Sing r -> () (bound at Bug.hs:27:1)
   |
29 |     Refl -> applySing no _
   |             ^^^^^^^^^^^^^^

Bug.hs:29:26: error:
    • Found hole: _ :: Sing t0
      Where: ‘t0’ is an ambiguous type variable
             ‘y’, ‘x’, ‘k’ are rigid type variables bound by
               the type signature for:
                 right :: forall k1 (x1 :: k1) (y1 :: k1) z (r :: (x1 :~: y1) ~> z).
                          Sing r -> ()
               at Bug.hs:(25,1)-(26,21)
    • In the second argument of ‘applySing’, namely ‘_’
      In the expression: applySing no _
      In a case alternative: Refl -> applySing no _
    • Relevant bindings include
        no :: Sing r (bound at Bug.hs:27:7)
        right :: Sing r -> () (bound at Bug.hs:27:1)
      Valid substitutions include
        undefined :: forall (a :: TYPE r).
                     GHC.Stack.Types.HasCallStack =>
                     a
          (imported from ‘Prelude’ at Bug.hs:7:8-10
           (and originally defined in ‘GHC.Err’))
   |
29 |     Refl -> applySing no _
   |                          ^

Note that this is distinct from #15142 (closed), as this is still reproducible on HEAD, even after commit 030211d2.

Trac metadata

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

changed milestone to %8.6.1

changed weight to 7

added Tbug Trac import typechecker typed holes labels

Simpler example:

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

import Data.Type.Equality

data S (a :: Either x y)

mkRefl :: n :~: j
mkRefl = Refl

right :: forall (r :: Either x y).
         S r -> ()
right no =
  case mkRefl @x @y of
    Refl -> no + _

This regression was introduced in commit e0b44e2e (Improved Valid Hole Fits).

assigned to @Tritlo

I'll get to work.

After some investigation, here is some more info:

I'm running this on the branch on which I've fixed #15384, and now it generates a different panic:

	Filling a filled coercion hole
  co_a1we
  Sym (S <x_a1vL[sk:1]>_N
         <x_a1vL[sk:1]>_N
         (Sym (GRefl nominal r_a1vN[sk:1]
                   (Sym (Either
                           <x_a1vL[sk:1]>_N (Sym co_a1vU))_N)) ; GRefl nominal r_a1vN[sk:1]
                                                                     (Sym (Either
                                                                             <x_a1vL[sk:1]>_N
                                                                             (Sym co_a1vU))_N)))_N ; {co_a1ws}
  Sym (S <x_a1vL[sk:1]>_N
         <x_a1vL[sk:1]>_N
         (Sym (GRefl nominal r_a1vN[sk:1]
                   (Sym (Either
                           <x_a1vL[sk:1]>_N (Sym co_a1vU))_N)) ; GRefl nominal r_a1vN[sk:1]
                                                                     (Sym (Either
                                                                             <x_a1vL[sk:1]>_N
                                                                             (Sym co_a1vU))_N)))_N ; {co_a1wm}

This happens when trying to simplify:

WC {wc_impl =
      Implic {
        TcLevel = 1
        Skolems = x_a1vL[sk:1]
                  y_a1vM[sk:1]
                  (r_a1vN[sk:1] :: Either x_a1vL[sk:1] y_a1vM[sk:1])
        No-eqs = True
        Status = Insoluble
        Given =
        Wanted =
          WC {wc_impl =
                Implic {
                  TcLevel = 2
                  Skolems =
                  No-eqs = False
                  Status = Insoluble
                  Given = co_a1vU :: y_a1vM[sk:1] GHC.Prim.~# x_a1vL[sk:1]
                  Wanted =
                    WC {wc_simple =
                          [WD] hole{co_a1wo} {0}:: (S r_a1vN[sk:1] -> ())
                                                   GHC.Prim.~# S (r_a1vN[sk:1] |> Sym (Either
                                                                                         <x_a1vL[sk:1]>_N
                                                                                         (Sym co_a1vU))_N) (CNonCanonical)
                          [WD] hole{co_a1we} {1}:: S (r_a1vN[sk:1] |> Sym (Either
                                                                             <x_a1vL[sk:1]>_N
                                                                             (Sym co_a1vU))_N)
                                                   GHC.Prim.~# () (CNonCanonical)
                          [WD] $dNum_a1wf {0}:: Num
                                                  (S (r_a1vN[sk:1] |> Sym (Either
                                                                             <x_a1vL[sk:1]>_N
                                                                             (Sym co_a1vU))_N)) (CNonCanonical)}
                  Binds = EvBindsVar<a1wp>
                  a pattern with constructor: Refl :: forall k (a :: k). a :~: a,
                  in a case alternative }}

where

WC {wc_simple =
    [WD] hole{co_a1wi} {0}:: y_a1vM[sk:1]
                                GHC.Prim.~# x_a1vL[sk:1] (CNonCanonical)}

is generated by tcSubType_NC.

I'm not sure how to prevent/catch the filling of the unfilled coercion hole and discard those fits.

Tritlo, what commit are you on? I just tried compiling the program in ticket:15370#comment:156689 using commit f0d27f51, and to my surprise, it no longer panics!

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

../Bug.hs:14:10: error:
    • Couldn't match type ‘n’ with ‘j’
      ‘n’ is a rigid type variable bound by
        the type signature for:
          mkRefl :: forall k (n :: k) (j :: k). n :~: j
        at ../Bug.hs:13:1-17
      ‘j’ is a rigid type variable bound by
        the type signature for:
          mkRefl :: forall k (n :: k) (j :: k). n :~: j
        at ../Bug.hs:13:1-17
      Expected type: n :~: j
        Actual type: n :~: n
    • In the expression: Refl
      In an equation for ‘mkRefl’: mkRefl = Refl
    • Relevant bindings include
        mkRefl :: n :~: j (bound at ../Bug.hs:14:1)
   |
14 | mkRefl = Refl
   |          ^^^^

../Bug.hs:20:13: error:
    • Couldn't match type ‘S r’ with ‘()’
      Expected type: ()
        Actual type: S r
    • In the expression: no + _
      In a case alternative: Refl -> no + _
      In the expression: case mkRefl @x @y of { Refl -> no + _ }
    • Relevant bindings include
        no :: S r (bound at ../Bug.hs:18:7)
        right :: S r -> () (bound at ../Bug.hs:18:1)
   |
20 |     Refl -> no + _
   |             ^^^^^^

../Bug.hs:20:18: error:
    • Found hole: _ :: S r
      Where: ‘r’, ‘y’, ‘x’ are rigid type variables bound by
               the type signature for:
                 right :: forall x y (r :: Either x y). S r -> ()
               at ../Bug.hs:(16,1)-(17,18)
    • In the second argument of ‘(+)’, namely ‘_’
      In the expression: no + _
      In a case alternative: Refl -> no + _
    • Relevant bindings include
        no :: S r (bound at ../Bug.hs:18:7)
        right :: S r -> () (bound at ../Bug.hs:18:1)
      Constraints include y ~ x (from ../Bug.hs:20:5-8)
   |
20 |     Refl -> no + _
   |                  ^

Which seems positive, although I'm not sure which commit would have fixed this.

I'm on a branch based on 973ff4a1, with the changes from b202e7a4 on top. In b202e7a4, I remove the call to tcTyVarLevel, which was calling tcTyVarDetails and causing the original panic. I suspect af624071, which I believe changes the hole{co_a1wi} {0}:: y_a1vM[sk:1] GHC.Prim.~# x_a1vL[sk:1] constraint that was causing the crash. I'll check to confirm.

I'm still getting the latter error on f0d27f51,when I build with the devel2 flavor (even after make distclean). Are you sure you're not seeing it RyanGlScott?

To be clear, is the error that you're experiencing in ticket:15370#comment:157212 an assertion failure, or a different form of panic? If it's the former, then that would explain why I'm not seeing it—I'm not using a devel* build flavor, so I don't have assertions enabled.

It's an assertion error. That would explain it.

I have a hypothesis about the assertion failure in ticket:15370#comment:157212

I see in TcHoleErrors.tcCheckHoleFit

     ; let w_rel_cts = addSimples wanted relevantCts
...
     ; let w_givens = foldr setWC w_rel_cts outermost_first
...
     ; rem <- runTcSDeriveds $ simpl_top w_givens

So the same relevantCts are used in multiple runs of runTcSDerived. You are careful to freshen the ic_binds of the implicatations, but if relevantCts contains any equalities they will have HoleDest, a coercion hole that is filled in directly. You really need to clone those holes too. Use TcMType.cloneWanted as in cloneWC.

As it happens, this cloneWanted is overkill, and I'm improving it in an upcoming patch, but for now I think it'll do what you need.

Does that make sense? Best to verify that this is indeed what is happening.

That was indeed what was happening. A fix is up on Phabricator (https://phabricator.haskell.org/D5004), including a regression test (the code from ticket:15370#comment:157212).

mentioned in commit 0dc86f6b

added 1 deleted label

Hmm, I'm afraid there is a piece that we are missing on ghc-8.6. T15370 fails with

ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.6.0.20180802 for x86_64-unknown-linux):
        tcTyVarDetails
  co_a1vS :: y_a1vK[sk:1] ~# x_a1vJ[sk:1]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
        pprPanic, called at compiler/basicTypes/Var.hs:497:22 in ghc:Var

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

when this is cherry-picked on ghc-8.6.

Tritlo, do you think you could look into this?

Yes. Does ghc-8.6 include b202e7a4 already? I think that resolved the original panic.

bgamari: It appears that the changes in b202e7a4 (which comes from https://phabricator.haskell.org/D4994) are not yet merged. If you merge that to ghc-8.6, it fixes the panic in T15370, and then https://phabricator.haskell.org/D5004 fixes the assertion that was being violated in DEBUG.

closed

ticket:15370#comment:157890 merged in f4e54330 and #15370 (closed) merged in 588364c3.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

removed 1 deleted label

added TypeInType label

added compiler crash label

added Phigh label