On Wednesday 24 April 2013, 18:34:07, gs wrote:
Daniel Fischer
writes: No, that is the catch:
undefined :: Source NotAnInstanceOfVariable Int
is possible.
OK, I've got that. Now let's say that
data Source v a = Variable v => Source {bindings :: v [Binding a], var :: v a} or data Variable v => Source v a = Source {bindings :: v [Binding a], var :: v a}
instance Variable (Source v) where newVar a = do bindings <- newVar [] v <- newVar a return $ Source bindings v
was allowed - then newVar (undefined :: Source NotAnInstanceOfVariable Int) would then attempt newVar (?? :: NotAnInstanceOfVariable), which doesn't type check, because newVar only works on Variables.
The type annotations here are wrong, since newVar :: a -> IO (v a) But yes, the problem is that the `newVar` implementation for `Source` uses the `newVar` implementation for `v`, hence newVar :: a -> IO (Source NotAnInstance Int) would be a type error. If the type was changed to newVar :: v a -> a -> IO (v a) newVar dummy value = old_implementation_ignoring_dummy you could write an instance Variable (Source v) where newVar (Source _ _) value = do binds <- newVar [] v <- newVar value return (Source binds v) with the GADT, since you get the Variable instance of the `v` parameter by pattern-matching on the dummy argument. For some Source NotAnInstance whatever type (such a type has no non-bottom values), `newVar` would be undefined.
Is this correct? If that's the only problem, it doesn't seem like much of a loss, as even with the type context, undefined :: Source SomeInstanceOfVariable Int isn't going to be of much use either.
The problem is that you can only write a useful instance if you can somehow access a useful Variable instance for the `v` parameter. Without an instance context or pattern-matching, the only possible implementations are variants of undefined.