Panic: generalised wildcards in RULES

Generalised wildcards (PartialTypeSignatures) in the binder type annotation of a RULE cause panics.

Minimal example:

module WildcardInRuleBndrSig where
{-# RULES
"map/empty" forall (f :: a -> _). map f [] = []
  #-}

Output:

WildcardInRuleBndrSig.hs:3:31:ghc-stage1: panic! (the 'impossible' happened)
  (GHC version 7.11.20150209 for x86_64-unknown-linux):
	No skolem info: w__alY[sk]

When a wildcard is generalised over, the error message reporting the inferred type gives some extra info about the type variables occurring in the inferred type. This extra information is retrieved by looking up the skolem information (getSkolemInfo) for the type variables in the enclosing implications (cec_encl). The problem is that there are no enclosing implications in this case, hence the panic.

Note that with the flags -XPartialTypeSignatures and -fno-warn-partial-type-signatures enabled, there is no panic, as no error/warning message is constructed.

Trac metadata

Trac field	Value
Version	7.10.1-rc2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import typechecker labels

Bug discovered while working on D613, where I also proposed an unsatisfactory stopgap solution: not printing extra skolem information when there is none.

We should never generalise over wildcards!

Thomas, are you ok to look into this one? Yell if you need help.

Simon

Replying to [ticket:10072#comment:96112 simonpj]:

We should never generalise over wildcards!

I'm confused, we do generalise over wildcards when possible, right? When I say "the wildcard is generalised over", I mean that when the wildcard is not instantiated to a monotype, we replace it with a fresh type variable and universally quantify it. This is what we have being doing the whole time, e.g.:

foo :: _ -> _
foo x = x
-- Inferred: w_ -> w_

What I expected in the example in the description above (and what indeed happens) is that the wildcard is generalised over and that we get a -> w_ as type for f.

Thomas, are you ok to look into this one? Yell if you need help.

I see two ways to solve it:

1. Don't print skolem information when there is none (easy).
2. Generate an Implication with the right skolem information (harder).

Which solution do you prefer? If you prefer 2, I'd appreciate some pointers as to where/when these Implication constraints should be generated.

mentioned in commit 5ab7518f

I think I have fixed this.

Probably worth merging to 7.10.

Simon

Trac metadata

Trac field	Value
Test case	→ typecheck/should_compile/T10072

added 1 deleted label

closed

changed milestone to %7.10.1

Merged to ghc-7.10 (via 20ccf726).

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

removed 1 deleted label

added compiler crash label

added Pnormal label