content: {-# LANGUAGE ScopedTypeVariables #-}
  {-@ LIQUID "--no-termination" @-}
  module Class () where
  
  import Language.Haskell.Liquid.Prelude
  import Prelude hiding (sum, length, (!!), Functor(..))
  -- import qualified Prelude as P
  
  {-@ qualif Size(v:Int, xs:a): v = size xs @-}
  
  {-@ qualif Size(v:Int, xs:MList a): v = size xs @-}
  
  {-@ data MList a = Nil | Cons (hd::a) (tl::(MList a)) @-}
  data MList a = Nil | Cons a (MList a)
  
  {-@ (!!) :: xs:MList a -> {v:Nat | v < (size xs)} -> a @-}
  (!!) :: MList a -> Int -> a
  Nil         !! _ = liquidError "impossible"
  (Cons x _)  !! 0 = x
  (Cons _ xs) !! i = xs !! (i - 1)
  
  {-@ class measure size :: forall a. a -> Int @-}
  
  {-@ class Sized s where
        size :: forall a. x:s a -> {v:Nat | v = size x}
    @-}
  class Sized s where
    size :: s a -> Int
  
  instance Sized MList where
    {-@ instance measure size :: MList a -> Int
          size Nil       = 0
          size (Cons x xs) = 1 + size xs
      @-}
    size = length
  
  {-@ length :: xs:MList a -> {v:Nat | v = size xs} @-}
  length :: MList a -> Int
  length Nil         = 0
  length (Cons _ xs) = 1 + length xs
  
  {-@ bob :: xs:MList a -> {v:Nat | v = size xs} @-}
  bob :: MList a -> Int
  bob = length
  
  
  instance Sized [] where
    {-@ instance measure size :: [a] -> Int
          size []   = 0
          size (x:xs) = 1 + (size xs)
      @-}
    size [] = 0
    size (_:xs) = 1 + size xs
  
  {-@ class (Sized s) => Indexable s where
        index :: forall a. x:s a -> {v:Nat | v < size x} -> a
    @-}
  class (Sized s) => Indexable s where
    index :: s a -> Int -> a
  
  
  instance Indexable MList where
    index = (!!)
  
  {-@ sum :: Indexable s => s Int -> Int @-}
  sum :: Indexable s => s Int -> Int
  sum xs = go max 0
    where
      max = size xs
      go (d::Int) i
        | i < max   = index xs i + go (d-1) (i+1)
        | otherwise = 0
  
  
  {-@ sumMList :: MList Int -> Int @-}
  sumMList :: MList Int -> Int
  sumMList xs = go max 0
    where
      max = size xs
      go (d::Int) i
        | i < max   = index xs i + go (d-1) (i+1)
        | otherwise = 0
  
  
  {-@ x :: {v:MList Int | (size v) = 3}  @-}
  x :: MList Int
  x = 1 `Cons` (2 `Cons` (3 `Cons` Nil))
  
  foo = liquidAssert $ size (Cons 1 Nil) == size [7]
  