#15625 closed bug (fixed)

GHC panic, with QuantifiedConstraints

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.6.1-beta1
Keywords: QuantifiedConstraints Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: quantified-constraints/T15625, T15625a
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by Iceland_jack)

I got a GHC Panic (I made some minor changes to GHC so it may have been added by me) but I think it's caused by the equality constraint

$ ~/code/latestghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci ~/hs/390.hs
GHCi, version 8.7.20180828: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( /home/baldur/hs/390.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.7.20180828 for x86_64-unknown-linux):
	ASSERT failed!
  co_a2DG
  df_a2DS @ Any
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
        pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable
        assertPprPanic, called at compiler/coreSyn/CoreSubst.hs:189:49 in ghc:CoreSubst

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

> 

given this code

{-# Language RankNTypes, TypeInType, DataKinds, PolyKinds, TypeOperators, GADTs, FlexibleInstances, MultiParamTypeClasses, ConstraintKinds, CPP, UndecidableSuperClasses, QuantifiedConstraints, FlexibleContexts #-}

import Data.Kind

type Cat ob = ob -> ob -> Type

data KLEISLI (m :: Type -> Type) :: Cat (KL_kind m) where
  MkKLEISLI :: (a -> m b) -> KLEISLI(m) (KL a) (KL b)

data KL_kind (m :: Type -> Type) = KL Type

class    (a ~ KL xx) => AsKL a xx
instance (a ~ KL xx) => AsKL a xx

ekki__ :: Monad m => (forall xx. AsKL a xx) => KLEISLI m a a
ekki__ = MkKLEISLI undefined 

Change History (7)

comment:1 Changed 12 months ago by RyanGlScott

If you don't have a GHC build with ASSERTions enabled, then it's worth noting that this program also triggers a Core Lint error:

$ /opt/ghc/8.6.1/bin/ghci Bug.hs -dcore-lint
GHCi, version 8.6.0.20180907: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/ryanglscott/.ghci
[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_a2KT :: HasCallStack]
    co_a2Lc :: a_a1Iw[sk:1] ~# 'KL Any
    [LclId[CoVarId]] is out of scope
*** Offending Program ***

<elided>

ekki__
  :: forall (m :: * -> *) (a :: KL_kind m).
     (Monad m, forall xx. AsKL a xx) =>
     KLEISLI m a a
[LclIdX]
ekki__
  = \ (@ (m_a1Iv :: * -> *))
      (@ (a_a1Iw :: KL_kind m_a1Iv))
      _ [Occ=Dead]
      (df_a1Iz :: forall xx. AsKL a_a1Iw xx) ->
      case \ (@ xx_a1Fp) ->
             heq_sel
               @ (KL_kind m_a1Iv)
               @ (KL_kind m_a1Iv)
               @ a_a1Iw
               @ ('KL xx_a1Fp)
               ($p1~
                  @ (KL_kind m_a1Iv)
                  @ a_a1Iw
                  @ ('KL xx_a1Fp)
                  ($p1AsKL @ m_a1Iv @ a_a1Iw @ xx_a1Fp (df_a1Iz @ xx_a1Fp)))
      of df_a2Lp
      { __DEFAULT ->
      let {
        $dIP_a2KT :: HasCallStack
        [LclId]
        $dIP_a2KT
          = (pushCallStack
               (unpackCString# "undefined"#,
                SrcLoc
                  (unpackCString# "main"#)
                  (unpackCString# "Main"#)
                  (unpackCString# "Bug.hs"#)
                  (I# 16#)
                  (I# 20#)
                  (I# 16#)
                  (I# 29#))
               ((emptyCallStack
                 `cast` (Sym (N:IP[0] <"callStack">_N <CallStack>_N)
                         :: CallStack ~R# (?callStack::CallStack)))
                `cast` (N:IP[0] <"callStack">_N <CallStack>_N
                        :: (?callStack::CallStack) ~R# CallStack)))
            `cast` (Sym (N:IP[0] <"callStack">_N <CallStack>_N)
                    :: CallStack ~R# (?callStack::CallStack)) } in
      (break<0>()
       $WMkKLEISLI
         @ Any
         @ m_a1Iv
         @ Any
         (undefined @ 'LiftedRep @ (Any -> m_a1Iv Any) $dIP_a2KT))
      `cast` ((KLEISLI <m_a1Iv>_N (Sym co_a2Lc) (Sym co_a2Lc))_R
              :: KLEISLI m_a1Iv ('KL Any) ('KL Any)
                 ~R# KLEISLI m_a1Iv a_a1Iw[sk:1] a_a1Iw[sk:1])
      }

comment:2 Changed 12 months ago by Iceland_jack

Description: modified (diff)

comment:3 Changed 12 months ago by monoidal

Simpler version that also gives Core Lint warning:

{-# Language GADTs, MultiParamTypeClasses, QuantifiedConstraints #-}

class a ~ b => Equal a b

ekki__ :: (forall b. Equal a b) => a
ekki__ = False

comment:4 Changed 12 months ago by Iceland_jack

[narrator] it was the equality constraint

thanks monoidal :] the purpose for this is to be able to write Control.Category.id of the form

id :: KLEISLI m (KL a) (KL a)
id = MkKLEISLI pure

but when we define

instance Category (KLEISLI m) where
  id :: KLEISLI m kl_a kl_a
  id = ..

GHC doesn't know that kl_a is of the form KL a (same as #7259) so I want to constraint the type signature of id by saying (forall a. kl_a ~ KL a).

But that is uncouth since it's "quantifying over constraints headed by (~)" (ticket:15593#comment:1)

comment:5 Changed 12 months ago by simonpj

Another, even simpler example, this time with Coercible

ekki__ :: (forall b. Coercible a b) => a
ekki__ = coerce False

The crash happens in the simple optimiser which optimises the output of desugarer, namelhy

ekki__ :: forall a. (forall b. Coercible * a b) => a
[LclIdX]
ekki__
  = \ (@ a_aWJ) (df_aWL :: forall b. Coercible * a_aWJ b) ->
      case \ (@ b_aW8) ->
             GHC.Types.coercible_sel @ * @ a_aWJ @ b_aW8 (df_aWL @ b_aW8)
      of df_aWU
      { __DEFAULT ->
      let {
        co_aWT :: (a_aWJ :: *) ~R# (Bool :: *)
        [LclId[CoVarId]]
        co_aWT = df_aWU @ Bool } in
      let {
        $dCoercible_aWO :: Coercible * Bool a_aWJ
        [LclId]
        $dCoercible_aWO
          = GHC.Types.MkCoercible
              @ *
              @ Bool
              @ a_aWJ
              @~ (Sym co_aWT :: (Bool :: *) ~R# (a_aWJ[sk:1] :: *)) } in
      coerce @ Bool @ a_aWJ $dCoercible_aWO GHC.Types.False
      }

The binding for co_aWT is unexpected (to GHC): it's a coercion (clearly) but it comes from applying an instance decl. The optimiser doesn't expect to see let-bound coercions, and that's what the ASSERT is spotting.

Last edited 12 months ago by simonpj (previous) (diff)

comment:6 Changed 12 months ago by Simon Peyton Jones <simonpj@…>

In bd76875a/ghc:

Allow (~) in the head of a quantified constraints

Since the introduction of quantified constraints, GHC has rejected
a quantified constraint with (~) in the head, thus
  f :: (forall a. blah => a ~ ty) => stuff

I am frankly dubious that this is ever useful.  But /is/ necessary for
Coercible (representation equality version of (~)) and it does no harm
to allow it for (~) as well.  Plus, our users are asking for it
(Trac #15359, #15625).

It was really only excluded by accident, so
this patch lifts the restriction. See TcCanonical
Note [Equality superclasses in quantified constraints]

There are a number of wrinkles:

* If the context of the quantified constraint is empty, we
  can get trouble when we get down to unboxed equality (a ~# b)
  or (a ~R# b), as Trac #15625 showed. This is even more of
  a corner case, but it produced an outright crash, so I elaborated
  the superclass machinery in TcCanonical.makeStrictSuperClasses
  to add a void argument in this case.  See
  Note [Equality superclasses in quantified constraints]

* The restriction on (~) was in TcValidity.checkValidInstHead.
  In lifting the restriction I discovered an old special case for
  (~), namely
      | clas_nm `elem` [ heqTyConName, eqTyConName]
      , nameModule clas_nm /= this_mod
  This was (solely) to support the strange instance
      instance a ~~ b => a ~ b
  in Data.Type.Equality. But happily that is no longer
  with us, since
     commit f265008fb6f70830e7e92ce563f6d83833cef071
     Refactor (~) to reduce the suerpclass stack
  So I removed the special case.

* I found that the Core invariants on when we could have
       co = <expr>
  were entirely not written down. (Getting this wrong ws
  the proximate source of the crash in Trac #15625.  So

  - Documented them better in CoreSyn
      Note [CoreSyn type and coercion invariant],
  - Modified CoreOpt and CoreLint to match
  - Modified CoreUtils.bindNonRec to match
  - Made MkCore.mkCoreLet use bindNonRec, rather
    than duplicate its logic
  - Made Simplify.rebuildCase case-to-let respect
      Note [CoreSyn type and coercion invariant],

comment:7 Changed 12 months ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: quantified-constraints/T15625, T15625a

Done!

Note: See TracTickets for help on using tickets.