Opened 11 days ago

Last modified 2 days ago

#15370 new bug

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 (4)

comment:1 Changed 11 days 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 11 days ago by RyanGlScott

Cc: Tritlo added

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

comment:3 Changed 10 days ago by Tritlo

Owner: set to Tritlo

I'll get to work.

comment:4 Changed 2 days 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.

Note: See TracTickets for help on using tickets.