variant xs :: List x where {
  cons :: x -> xs -> xs;
  nil  :: xs
}
;

variant xs :: List x => xs :: List2 x where {
  cons2 :: x -> x -> xs -> xs
}
;

variant xs :: List x => xs :: AppendList x where {
  append :: xs -> xs -> xs
}
;


record xs :: ListAcceptor x where {
  toListView :: xs -> Either (x, xs) ()
}
;

instance List x :: xs :: ListAcceptor x where {
  toListView (cons x xs) = Left (x, xs);
  toListView nil         = Right ()
}
;

isNullView (Right ())     = True;
isNullView (Left (x, xs)) = False;
isNull = isNullView . toListView;

hdView (Left (x, xs)) = x;
hd = hdView . toListView;

tlView (Left (x, xs)) = xs;
tl = tlView . toListView;

myLengthView (Right ())     = 0;  
myLengthView (Left (x, xs)) = 1 + myLength xs;
myLength = myLengthView . toListView;

instance List2 x :: xs :: ListAcceptor x where {
  toListView (cons2 x1 x2 xs) = toListView (cons x1 (cons x2 xs)) 
}
;

instance AppendList x :: xs :: ListAcceptor x where {
  toListView (append xs ys) = toListView (if isNull xs then ys else cons (hd xs) (append (tl xs) ys));
}
;

x = 1; 
xs = cons2 (2 * 1) (x+1) nil;
ys = append xs xs;
baz = myLength ys;
qux a = myLength (append (cons2 a a nil) nil);
;


{-

Because we cannot turn off ``monomorphism restriction'' in Hugs,
we must add some explicit type signatures to the output of this example.

isNull :: ListAcceptor xs x => xs -> Bool;
hd :: ListAcceptor xs x => xs -> x;
tl :: ListAcceptor xs x => xs -> xs;
ys :: (AppendList xs Integer, List2 xs Integer) => xs;
xs :: List2 xs Integer => xs;
myLength :: ListAcceptor xs x => xs -> Integer;

-}