Opened 3 years ago

Closed 3 years ago

Last modified 3 years ago

#13381 closed bug (fixed)

"opt_univ fell into a hole" panic from rewrite rule

Reported by: dfeuer Owned by:
Priority: normal Milestone: 8.2.1
Component: Compiler Version: 8.1
Keywords: Cc: roboguy, goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash or panic Test Case: typecheck/should_compile/T13381
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Roboguy reports (via IRC) that the following causes a GHC panic:

{-# LANGUAGE RankNTypes #-}

module Crash where

data Exp a = Exp

fromExp :: Exp a -> a
fromExp _ = error "Impossible"

toExp :: a -> Exp a
toExp _ = Exp



newtype Iter a b = Iter { getIter :: forall r. (a -> r) -> (b -> r) -> r }

iterLoop :: (a -> Iter a b) -> a -> b
iterLoop f x = getIter (f x) (iterLoop f) id


  -- This rewrite rule results in a GHC panic: "opt_univ fell into a hole" on GHC 8.0.1, 8.0.2, and 8.1.
{-# RULES "fromExp-into-iterLoop" [~]
    forall (f :: Int -> Iter (Exp Int) (Exp Char))
           (init :: Int).
    fromExp (iterLoop f init)
      =
    fromExp (iterLoop (f . fromExp) (toExp init))
  #-}

I have confirmed this, and see the following error:

ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.1.20170305 for x86_64-unknown-linux):
        opt_univ fell into a hole
  {a1WD}
  Call stack:
      CallStack (from HasCallStack):
        prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1191:58 in ghc:Outputable
        callStackDoc, called at compiler/utils/Outputable.hs:1195:37 in ghc:Outputable
        pprPanic, called at compiler/types/OptCoercion.hs:398:29 in ghc:OptCoercion

Change History (6)

comment:1 Changed 3 years ago by RyanGlScott

To make things even more interesting, this error does not occur on GHC 7.8 or 7.10. Here's the error you get with 7.10.3:

GHCi, version 7.10.3: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Crash            ( Bug.hs, interpreted )

Bug.hs:25:23:
    Couldn't match type ‘Exp Int’ with ‘Int’
    Expected type: Exp Int -> Iter (Exp Int) (Exp Char)
      Actual type: Int -> Iter (Exp Int) (Exp Char)
    In the first argument of ‘iterLoop’, namely ‘f’
    In the first argument of ‘fromExp’, namely ‘(iterLoop f init)’

Bug.hs:25:25:
    Couldn't match expected type ‘Exp Int’ with actual type ‘Int’
    In the second argument of ‘iterLoop’, namely ‘init’
    In the first argument of ‘fromExp’, namely ‘(iterLoop f init)’

comment:2 Changed 3 years ago by RyanGlScott

Cc: goldfire added

Commit 6746549772c5cc0ac66c0fce562f297f4d4b80a2 (Add kind equalities to GHC) introduced this regression.

comment:3 Changed 3 years ago by goldfire

To be clear, the opt_univ fell into a hole bit is a red herring here. The real problem is that the type-checker doesn't reject the program.

comment:4 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In af6ed4a6/ghc:

Fix constraint simplification in rules

Trac #13381 showed that we were losing track of a wanted constraint
when simplifying the LHS constraints for a RULE.

This patch fixes it, makes the code a bit simpler, and better
documented.

comment:5 Changed 3 years ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: typecheck/should_compile/T13381

comment:6 Changed 3 years ago by bgamari

Note: See TracTickets for help on using tickets.