content: {-@ LIQUID "--expect-any-error" @-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-@ LIQUID "--no-termination" @-}
  module Class1 () where
  
  import Language.Haskell.Liquid.Prelude
  import Prelude hiding (sum, length, (!!), Functor(..))
  import qualified Prelude as P
  
  {-@ qualif Sz(v:int, xs:a): v = (sz xs) @-}
  
  {-@ data List a = Nil | Cons (hd::a) (tl::(List a)) @-}
  data List a = Nil | Cons a (List a)
  
  {-@ length :: xs:List a -> {v:Nat | v = (sz xs)} @-}
  length :: List a -> Int
  length Nil         = 0
  length (Cons x xs) = 1 + length xs
  
  {-@ (!!) :: xs:List a -> {v:Nat | v < (sz xs)} -> a @-}
  (!!) :: List a -> Int -> a
  Nil         !! i = undefined
  (Cons x _)  !! 0 = x
  (Cons x xs) !! i = xs !! (i - 1)
  
  {-@ class measure sz :: forall a. a -> Int @-}
  {-@ class Sized s where
        size :: forall a. x:s a -> {v:Nat | v = (sz x)}
    @-}
  class Sized s where
    size :: s a -> Int
  
  instance Sized List where
    {-@ instance measure sz :: List a -> Int
          sz (Nil)       = 0
          sz (Cons x xs) = 1 + (sz xs)
      @-}
    size = length
  
  {-@ class (Sized s) => Indexable s where
        index :: forall a. x:s a -> {v:Nat | v < (sz x)} -> a
    @-}
  class (Sized s) => Indexable s where
    index :: s a -> Int -> a
  
  
  instance Indexable List 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 = index xs i -- should be 0
  
  
  {-@ sumList :: List Int -> Int @-}
  sumList :: List Int -> Int
  sumList xs = go max 0
    where
      max = size xs
      go (d::Int) i
        | i < max   = index xs i + go (d-1) (i+1)
        | otherwise = index xs i -- should be 0
  
  
  