Opened 5 years ago

Closed 5 years ago

#10072 closed bug (fixed)

Panic: generalised wildcards in RULES

Reported by: thomasw Owned by: thomasw
Priority: normal Milestone: 7.10.1
Component: Compiler (Type checker) Version: 7.10.1-rc2
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash Test Case: typecheck/should_compile/T10072
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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.

Change History (6)

comment:1 Changed 5 years ago by thomasw

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

comment:2 Changed 5 years ago by simonpj

We should never generalise over wildcards!

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

Simon

comment:3 in reply to:  2 Changed 5 years ago by thomasw

Replying to 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.

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

In 5ab7518f28e89515c73ff09acd48b5acab48b8a5/ghc:

Improve typechecking of RULEs, to account for type wildcard holes

This fixes Trac #10072. Previously the type-hole constraint was
escaping to top level, but it belongs in the scope of the skolems
bound by the RULE.

comment:5 Changed 5 years ago by simonpj

Status: newmerge
Test Case: typecheck/should_compile/T10072

I think I have fixed this.

Probably worth merging to 7.10.

Simon

comment:6 Changed 5 years ago by thoughtpolice

Milestone: 7.10.1
Resolution: fixed
Status: mergeclosed

Merged to ghc-7.10 (via 20ccf72614bab9a00767b2514b7cded4b6e3084e).

Note: See TracTickets for help on using tickets.