Assertion failure with ExistentialQuantification and ApplicativeDo

{-# LANGUAGE ExistentialQuantification, ApplicativeDo #-}

module Bug where

data T f = forall a. MkT (f a)

runf :: forall f. Functor f => IO (T f)
runf = do
    return ()
    MkT fa <- runf
    return $ MkT fa

Bug.hs:11:18: error:ghc: panic! (the 'impossible' happened)
  (GHC version 8.6.3 for x86_64-unknown-linux):
	No skolem info:
  [a_a1nb[ssk:2]]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
        pprPanic, called at compiler/typecheck/TcErrors.hs:2891:5 in ghc:TcErrors

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

changed weight to 5

added Tbug Trac import labels

changed the description

added ApplicativeDo label

I think the root cause of this is that the applicative-do stuff just doesn't work well with existentials. See the paper. The desugaring in Fig 5 really only works if the binder of the patterns don't include existentials.

To me that says:

• GHC should check for this and complain if necessary. Not crash!
• Someone might like to think about whether it'd be possible to accommodate existentials.

Simon M: this is your territory.

added compiler crash label

added Pnormal label

added No skolem info label

I can't reproduce this with HEAD anymore. Closing optimistically.

closed

Did you add a regression test?

Reopening since this results the following assertion failure with the devel2 compiler:

  GHC version 9.3.20210628:
	ASSERT failed!
  2
  1
  a_aEl[tau:1]
  a_aE7[ssk:2]
  Call stack:
      CallStack (from HasCallStack):
        massertPpr, called at compiler/GHC/Tc/Utils/TcMType.hs:1006:10 in ghc:GHC.Tc.Utils.TcMType

reopened

mentioned in merge request !6097 (merged)

The assertion still fails here with !7105 (closed), I think Simon is right that the issue is that ApplicativeDo and existentials don't work well together.

changed title from Panic with ExistentialQuantification and ApplicativeDo to Assertion failure with ExistentialQuantification and ApplicativeDo

removed No skolem info label

This test exposes an ouright bug in GHC, which leads to an assertion error as above. It would be great if someone who cares about ApplicativeDo could add a test for existentials (which aren't supported) so we got a decent error message rather than bogus results.

When assertions are not on, the program compiles -- probably wrongly.

With my new constraint solver !10123 (merged) it generates a type error in a compiler with assertions off. Maybe that's better, I'm not sure. But the same assertion fails if assertions are on.

mentioned in issue #21116 (closed)

Looks like do to RebindableSyntax + ApplicativeDo via HsExpansion, (#24406), this will type-check. Can someone confirm that it should typecheck?

mentioned in commit 67ee05e6

mentioned in commit 65ae9818

mentioned in commit fbf2bfa6

mentioned in commit 243a394c

mentioned in commit 0ca8571c

mentioned in commit 468c413e

mentioned in commit 0dd8fb6b

mentioned in commit 4d2c7110

mentioned in commit 23338b91

mentioned in commit 96f76d93

mentioned in commit 6575ca67

mentioned in commit 8a753de0

mentioned in commit 57d640c5

mentioned in commit 0a862888

mentioned in commit 717874a0

mentioned in commit 73091d9e

mentioned in commit 96628d99

mentioned in commit 65d08ae5

mentioned in commit 0115a150

mentioned in commit 8b41cec3

mentioned in commit e359a879

mentioned in commit e683f8d2

mentioned in commit 66e8a1c6

mentioned in commit 731dd45a

mentioned in commit 6ae95217

mentioned in commit c4e6483e

mentioned in commit c533d25f

mentioned in commit 5be55c1f

mentioned in commit be1424c0

mentioned in commit 709bb3a3

mentioned in commit da545574

mentioned in commit 1b36ade3

mentioned in commit deb5e0a6

mentioned in commit 491e075b

mentioned in commit f44ed71c

mentioned in commit 6e34c0e2

mentioned in commit ffc711d2