24 Sep
2008
24 Sep
'08
2:26 p.m.
This has never worked with fundeps, because it involves a *local* type equality (one that holds in some places and not others) and my implementation of fundeps is fundamentally based on *global* equality. Prior to GADTs that was fine!
Actually, how does that relate to reasoning under assumptions? class FD a b | a -> b f :: (FD t1 t2, FD t1 t3) => .. f = .. There is no instance of 'FD', so no equalities can be derived from there outside of 'f', and no equalities should be derived globally from instances that are only local hypotheses in 'f' . But inside 'f', we assume that those two 'FD' instances exist, so we should assume 't2 ~ t3' to the right of the implication. Isn't that decidedly local? Claus