Opened 12 months ago

Closed 11 months ago

Last modified 5 months ago

#9161 closed bug (fixed)

Pattern synonyms interact badly with data kinds

Reported by: Iceland_jack Owned by: cactus
Priority: lowest Milestone: 7.8.3
Component: Compiler (Type checker) Version: 7.8.2
Keywords: renamer, PatternSynonyms, data kinds Cc: cactus
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash Test Case:
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description

If we define a pattern A and use it as a type:

{-# LANGUAGE PatternSynonyms, DataKinds #-}

pattern A = ()

b :: A
b = undefined

we get the following error:

Prelude> :load tmp.XDGqzccOAV.hs
[1 of 1] Compiling Main             ( /tmp/tmp.XDGqzccOAV.hs, interpreted )

/tmp/tmp.XDGqzccOAV.hs:5:9:
    GHC internal error: ‘A’ is not in scope during type checking, but it passed the renamer
    tcl_env of environment: []
    In the type signature for ‘blah’: blah :: A
Failed, modules loaded: none.

Also occurs with different arities of A (the arity of the pattern and type can differ) and defining it as an operator (enabling the TypeOperators pragma).

Change History (10)

comment:1 Changed 12 months ago by simonpj

  • Cc cactus added
  • Owner set to cactus

Probably we should not promote pattern synonyms to the type level, so the program should be rejected with "you can't use a pattern synonym as a type, even with DataKinds" error.

Gergo might you look at this?

Simon

comment:2 Changed 12 months ago by cactus

  • Component changed from Compiler to Compiler (Type checker)
  • Operating System changed from Linux to Unknown/Multiple
  • Type of failure changed from None/Unknown to Compile-time crash

This one is tricky...

One would expect in this scenario roughly the same code path as if you write

{-# LANGUAGE DataKinds #-}
data TYPE = CON

wrongLift :: CON
wrongLift = undefined

which BTW results in a reasonable error message:

Expected a type, but ‘CON’ has kind ‘TYPE’
In the type signature for ‘wrongLift’: wrongLift :: CON

However, since pattern synonyms are internally handled as binds, not TyClDecls, they are not yet in scope during kind checking (which is done by tcTyClsInstDecls) - hence the crash.

How do we even get to trying to kindcheck them? OccName.demoteOccName handles data constructor names and type constructor names the same way, since we don't differentiate between the two there.

So I think our best bet would be to have a bespoke internal kind for pattern synonyms, inject pattern synonyms at that kind before doing kind checking, and then barf on types of that kind with a meaningful error message.

Simon, does that sound like a good plan of action?

comment:3 Changed 12 months ago by simonpj

Basically yes. I suggest one of two things:

  • Add pattern synonyms as AGlobal (AConLike (PatSynCon (panic "..."))). Apart from the panic, this is exactly how imported pattern synonyms will appear, and TcHsType.tcTyVar will call wrongThingErr on it. It would make sense for local pattern synonmys to behave the same way. The panic won't be looked at because TcEnv.wrongThingErr doesn't look at the payload.
  • Short cut: don't extend the environment. Instead, in the "no in scope during type checking" error, test for DataName and instead complain about using a pattern synonym in a type. Better: do this only in the context of tcTyVar, by replicating a certain amount of the tcLookup code. This is bit of a hack; I'd rather not do it.

Simon

comment:4 Changed 11 months ago by cactus

  • Status changed from new to merge

comment:5 Changed 11 months ago by cactus

Fixed using Simon's approach #1.

comment:6 Changed 11 months ago by simonpj

The actual commit is

commit aa3166f42361cb605e046f4a063be3f9e1f48015
Author: Dr. ERDI Gergo <[email protected]>
Date:   Sat Jun 21 22:37:50 2014 +0800

    Add fake entries into the global kind environment for pattern synonyms.
    
    This is needed to give meaningful error messages (instead of internal
    panics) when a program tries to lift a pattern synonym into a kind.
    (fixes T9161)


>---------------------------------------------------------------

aa3166f42361cb605e046f4a063be3f9e1f48015
 compiler/typecheck/TcBinds.lhs                    | 23 ++++++++++++++++-------
 compiler/typecheck/TcHsType.lhs                   |  1 -
 testsuite/tests/patsyn/should_fail/T9161-1.hs     |  7 +++++++
 testsuite/tests/patsyn/should_fail/T9161-1.stderr |  4 ++++
 testsuite/tests/patsyn/should_fail/T9161-2.hs     |  9 +++++++++
 testsuite/tests/patsyn/should_fail/T9161-2.stderr |  5 +++++
 testsuite/tests/patsyn/should_fail/all.T          |  2 ++
 7 files changed, 43 insertions(+), 8 deletions(-)

comment:7 Changed 11 months ago by Simon Peyton Jones <simonpj@…>

In 0757831eaca96c8ebfd99fc51427560d3568cffa/ghc:

Add Note [Placeholder PatSyn kinds] in TcBinds

This is just documentation for the fix to Trac #9161

comment:8 Changed 11 months ago by cactus

Thanks for that note, which explains it much better than my original comment.

comment:9 Changed 11 months ago by thoughtpolice

  • Milestone set to 7.8.3
  • Resolution set to fixed
  • Status changed from merge to closed

This was merged into GHC 7.8 for 7.8.3 (part of fixing #9175).

comment:10 Changed 5 months ago by cactus

  • Keywords PatternSynonyms added; pattern synonyms removed
Note: See TracTickets for help on using tickets.