[Haskell-beginners] How to avoid repeating a type restriction from a data constructor

[Daniel Fischer]

On Wednesday 24 April 2013, 18:34:07, gs wrote:
> Daniel Fischer <daniel.is.fischer <at> googlemail.com> 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.