can newtype be extended to permit GADT-like declarations

[nr]

I'd like to create the following value constructor without the overhead of data:

data B n e x where
  B :: Body n -> B n C C

However, if I ask for newtype instead of data I'm told that a newtype constructor must have a return type of form T a1 ... an. Is this restriction fundamental? If not, could it be possible to allow GADT-like declarations for newtype?

[simonpj]

It's fundamental. Suppose we had

data T a where
   MkT :: Int -> T Int

f :: T a -> a -> Int
f (MkT n) m = m+1

blah = f (MkT 4) 6          -- Calling f at type Int, works
boo  = f (error "urk") True -- Calling f at type True, diverges

This is fine. Matching on the MkT ensures that a~Int. The call in blah is fine, and returns 7. The call in boo also type-checks fine, but the pattern match in f will diverge, so we won't get a seg fault when we try to evaluate True + 1.

But if instead we had

newtype T a where
   MkT :: Int -> T Int

f :: T a -> a -> Int
f (MkT n) m = m+1

blah = f (MkT 4) 6          -- Calling f at type Int, works
boo  = f (error "urk") True -- Calling f at type True, diverges

Now we would get a seg-fault by evaluating True + 1. The point is that matching against the MkT constructor does no evaluation.

A System-FC way of saying this is that matching against a data constructor brings into scope an equality coercion variable; but "matching" against a newtype constructor doesn't, and can't.

Simon