type families + GADT = type unsafety?

2007-09-20 Thread Roberto Zunino
(Trac reports "database locked", posting here...) Here's unsafeCoerce: > type family Const a > type instance Const a = () > > data T a where T :: a -> T (Const a) > > coerce :: forall a b . a -> b > coerce x = case T x :: T (Const b) of >T y -> y And this indeed "works"... Here's t

Re: type families + GADT = type unsafety?

2007-09-27 Thread Roberto Zunino
Roberto Zunino wrote: (Trac reports "database locked", posting here...) For those interested, here are the follow-ups: http://hackage.haskell.org/trac/ghc/ticket/1723 Regards, Zun. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell

Re: type families + GADT = type unsafety?

2007-09-27 Thread Wolfgang Jeltsch
Am Donnerstag, 27. September 2007 15:27 schrieb Roberto Zunino: > Roberto Zunino wrote: > > (Trac reports "database locked", posting here...) > > For those interested, here are the follow-ups: > > http://hackage.haskell.org/trac/ghc/ticket/1723 > > Regards, > Zun. simonpj writes there: > Manuel is

RE: type families + GADT = type unsafety?

2007-09-27 Thread Simon Peyton-Jones
| | simonpj writes there: | > Manuel is about to nuke the old GADT stuff in favour of the new type- | family | > stuff. | | This doesn’t mean that GADTs are being dropped in favor of type | families, does | it? | No... it's an implementation matter only, invisible to programmers Simon ___

Re: type families + GADT = type unsafety?

2007-09-27 Thread Stefan O'Rear
On Thu, Sep 27, 2007 at 04:59:49PM +0200, Wolfgang Jeltsch wrote: > Am Donnerstag, 27. September 2007 15:27 schrieb Roberto Zunino: > > Roberto Zunino wrote: > > > (Trac reports "database locked", posting here...) > > > > For those interested, here are the follow-ups: > > > > http://hackage.haskell

Re: type families + GADT = type unsafety?

2007-09-27 Thread Tom Schrijvers
(Simon, does this mean that non-~ discharging will become subject to GADT-style type annotation rules?) No, it does not. No type annotations required in non-GADT-related code, even if equalities are involved. Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 2

Re[2]: type families + GADT = type unsafety?

2007-09-28 Thread Bulat Ziganshin
Hello Stefan, Friday, September 28, 2007, 1:10:09 AM, you wrote: > data Foo a where >A :: Foo Int >B :: Foo Bool > becomes > data Foo a = (a ~ Int) => A | (a ~ Bool) => B hm :) this looks like my quasi-proposal of unifying data and function definitions still has some meaning. i propos