#4009: can newtype be extended to permit GADT-like declarations
--------------------------------------+-------------------------------------
Reporter: nr | Owner: simonpj
Type: feature request | Status: closed
Priority: normal | Milestone: 6.14.1
Component: Compiler (Type checker) | Version: 6.12.1
Resolution: invalid | Keywords: newtype GADT
Difficulty: | Os: Linux
Testcase: | Architecture: x86
Failure: None/Unknown |
--------------------------------------+-------------------------------------
Changes (by simonpj):
* status: new => closed
* resolution: => invalid
Comment:
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
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4009#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
