Opened 7 years ago

Closed 7 years ago

Last modified 7 years ago

#7156 closed bug (fixed)

"Pattern match on GADT" error for non-GADT

Reported by: ryani Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.0.4
Keywords: GADTs, TypeFamilies, ExistentialQuantification Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: indexed-types/should_compile/T7156
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

It's widely known that GADTs are just generalizations of type equality and existentials. And you can declare them that way!

{-# LANGUAGE TypeFamilies, ExistentialQuantification #-}
module NonGADT where
data T a = (a ~ ()) -> T

But pattern matching on this gives a nasty error!

f :: T a -> a
f T = ()
{-
NonGADT.hs:7:3:
    A pattern match on a GADT requires -XGADTs
    In the pattern: T
    In an equation for `f': f T = ()
 -}

Attachments (1)

NonGADT.hs (137 bytes) - added by ryani 7 years ago.
File that fails to compile

Download all attachments as: .zip

Change History (10)

Changed 7 years ago by ryani

Attachment: NonGADT.hs added

File that fails to compile

comment:1 Changed 7 years ago by ryani

Minor typo in bug submission:

data T a = (a ~ ()) => T

It's correct in the attachment.

comment:2 Changed 7 years ago by simonpj

difficulty: Unknown

Urgh. I'm not sure what you really want to happen here. Do you want a different error message depending on the syntax used when T was declared? Or, since g doesn't use any strange syntax, do you want it to be accepted without any flags at all? Or do you want the error message to be worded differently? It's not very clear to me.

comment:3 Changed 7 years ago by ryani

I expect that if you can define a data type with particular extensions, you should be able to pattern match on that data type successfully. Or else, what's the point of defining it? This is a failure in a single module, not two modules defined with different extensions, which surprised me!

There extensions being used here, EqualityConstraints (via TypeFamilies) and ExistentialQuantification, are well known to be equivalent in power to GADTs in defining types. But, I guess there is extra type system machinery to deal with the T a -> a vs T a -> () problem that is currently only enabled with GADTs?

It seems like equality constraints require that same machinery; at least if they are able to be brought into scope via pattern matching.

comment:4 Changed 7 years ago by ryani

Interesting workaround I just found...

{-# LANGUAGE TypeFamilies, ExistentialQuantification #-}
module NonGADT where

class (a ~ ()) => C a
instance C ()

data T a = (C a) => T
f :: T a -> a
f T = ()

typechecks successfully under GHC7.4.1. It seems to work identically to GADTs, including inferring the type of T as T () .

comment:5 Changed 7 years ago by simonpj

What change, concretely, do you propose?

comment:6 Changed 7 years ago by ryani

I propose "f should typecheck successfully". Even more concretely, I propose that the TypeFamilies extension (which enables equality constraints, correct?) should enable pattern matching on types that otherwise appear to be GADTs.

comment:7 Changed 7 years ago by simonpj@…

commit 3eb6e211dec006f3609dd880cbef83ee2ad719de

Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Mon Aug 20 14:28:00 2012 +0100

    When pattern matching against a constructor with equalities,
    require either -XGADTs *or* -XTypeFamilies (rather than only the former)
    
    Fixes Trac #7156

 compiler/typecheck/TcPat.lhs |   10 ++++++----
 1 files changed, 6 insertions(+), 4 deletions(-)

comment:8 Changed 7 years ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: indexed-types/should_compile/T7156

OK, done.

comment:9 Changed 7 years ago by ryani

Thanks Simon!

Note: See TracTickets for help on using tickets.