{-# LANGUAGE ScopedTypeVariables #-}
{-@ LIQUID "--no-termination" @-}
module Class () where

import Language.Haskell.Liquid.Prelude

{-@ 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 [] where
  {-@ instance measure sz :: [a] -> Int
      sz ([])   = 0
      sz (x:xs) = 1 + (sz xs)
    @-}
  size []     = 0
  size (x:xs) = 1 + size xs

{-@ 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 [] where
  index = (!!)