Opened 6 years ago

Closed 6 years ago

#2516 closed bug (duplicate)

Panic in typechecker when checking rules

Reported by: josef Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 6.8.2
Keywords: Cc:
Operating System: Linux Architecture: x86
Type of failure: Difficulty: Unknown
Test Case: Blocked By:
Blocking: Related Tickets:

Description

GHC will panic when given either of the following modules. The error messages are somewhat different for the two different rules.

module GHCBug1 where

foo :: (forall a . a -> f a) -> f Int
foo f = f undefined

{-# RULES
    "bug1"
    forall (g :: a -> f a) .
    head (foo g) = undefined
 #-}
module GHCBug2 where

foo :: (forall a . a -> f a) -> f Int
foo f = f undefined

{-# RULES
    "bug2"
    forall (g :: forall a . a -> f a) .
    head (foo g) = undefined
 #-}

Change History (1)

comment:1 Changed 6 years ago by simonpj

  • Difficulty set to Unknown
  • Resolution set to duplicate
  • Status changed from new to closed

Several things going on here. First, I've already fixed a bug in typechecking for rules, so it doesn't crash any more. Second, see #2497; you need -XScopedTypeVariables -XRankNTypes -XPatternSignatures; that will improve shortly. At that point, with the HEAD and those flags we get:

T2516.hs:9:15:
    Couldn't match expected type `[]' against inferred type `f'
      `f' is a rigid type variable bound by
          the type signature for `g' at T2516.hs:8:23
    In the first argument of `foo', namely `g'
    In the first argument of `head', namely `(foo g)'
    When checking the transformation rule "bug1"

T2516.hs:9:15:
    Couldn't match expected type `a1' against inferred type `a'
      `a1' is a rigid type variable bound by
           the polymorphic type `forall a1. a1 -> [a1]' at T2516.hs:9:11
      `a' is a rigid type variable bound by
          the type signature for `g' at T2516.hs:8:18
    In the first argument of `foo', namely `g'
    In the first argument of `head', namely `(foo g)'
    When checking the transformation rule "bug1"

And indeed that's right. What you wanted in GHCBug1 is this:

{-# RULES
    "bug1"
    forall (g :: forall a. a -> [a]) .
    head (foo g) = undefined
 #-}

Note the forall in the type of g, and the [a] instead of f a. Then all is cool.

So I'll close this as a dup of #2497.

Simon

Note: See TracTickets for help on using tickets.