Opened 2 months ago

Closed 6 weeks ago

#15370 closed bug (fixed)

Typed hole panic on GHC 8.6 (tcTyVarDetails)

Reported by: RyanGlScott Owned by: Tritlo
Priority: high Milestone: 8.6.1
Component: Compiler (Type checker) Version: 8.4.3
Keywords: TypeInType, TypedHoles Cc: Tritlo
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

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, as this is still reproducible on HEAD, even after commit 030211d21207dabb7a4bf21cc9af6fa5eb066db1.

Change History (18)

comment:1 Changed 2 months ago by RyanGlScott

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 + _

comment:2 Changed 2 months ago by RyanGlScott

Cc: Tritlo added

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

comment:3 Changed 2 months ago by Tritlo

Owner: set to Tritlo

I'll get to work.

comment:4 Changed 2 months ago by Tritlo

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.

comment:5 Changed 2 months ago by RyanGlScott

Tritlo, what commit are you on? I just tried compiling the program in comment:1 using commit f0d27f515ffbc476144d1d1dd1a71bf9fa93c94b, 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.

comment:6 Changed 2 months ago by Tritlo

I'm on a branch based on 973ff4a142e77e247caebf828aa51f9810394938, with the changes from b202e7a48401bd8e805a92dcfe5ea059cbd8e41c on top. In b202e7a4, I remove the call to tcTyVarLevel, which was calling tcTyVarDetails and causing the original panic. I suspect af624071fa063158d6e963e171280676f9c0a0b0, 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.

comment:7 Changed 2 months ago by Tritlo

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

comment:8 Changed 2 months ago by RyanGlScott

To be clear, is the error that you're experiencing in comment:4 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.

comment:9 Changed 2 months ago by Tritlo

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

comment:10 Changed 2 months ago by simonpj

I have a hypothesis about the assertion failure in comment:4

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.

comment:11 Changed 2 months ago by Tritlo

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

comment:12 Changed 2 months ago by Tritlo

Status: newpatch

comment:13 Changed 2 months ago by Krzysztof Gogolewski <krz.gogolewski@…>

In 0dc86f6b/ghc:

Clone relevant constraints to avoid side-effects on HoleDests. Fixes #15370.

Summary: When looking for valid hole fits, the constraints relevant
to the hole may sometimes contain a HoleDest. Previously,
these were not cloned, which could cause the filling of filled
coercion hole being, which would cause an assert to fail. This is now fixed.

Test Plan: Regression test included.

Reviewers: simonpj, bgamari, goldfire

Reviewed By: simonpj

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #15370

Differential Revision: https://phabricator.haskell.org/D5004

comment:14 Changed 2 months ago by monoidal

Status: patchmerge

comment:15 Changed 7 weeks ago by bgamari

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?

comment:16 Changed 7 weeks ago by Tritlo

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

comment:17 Changed 7 weeks ago by Tritlo

bgamari: It appears that the changes in b202e7a48401bd8e805a92dcfe5ea059cbd8e41c (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.

Last edited 7 weeks ago by Tritlo (previous) (diff)

comment:18 Changed 6 weeks ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.