Towards Idris Version 1.0(idris-lang.org)

    data Union :: [Type] -> Type -> Type where
      ...

    data Free :: (Type -> Type) -> Type -> Type where
      ...
    
    type Eff fs = Free (Union fs)
    
    class Inject f fs where
      inj :: f a -> Union fs a
    
    data File :: Type -> Type where
      Open :: FilePath -> File ()
      Close :: FilePath -> File ()
    
    send :: (Inject f fs) => f a -> Eff fs a
    
    -- The inferred type would be more general
    openClose :: Eff '[File] ()
    openClose = do
      send (Open "foo.txt")
      send (Close "foo.txt")

    data HList :: [Type] -> Type where
      Nil :: HList '[]
      (:>) :: a -> HList as -> HList (a ': as)

    data Union :: HList fs -> HList is -> HList is -> Type -> Type where
      ...

    data Free :: (is -> is -> Type -> Type) -> is -> is -> Type -> Type where
      ...
    
    type Eff fs = Free (Union fs)
    
    class Inject f i o fs is os where
      inj :: f i o a -> Union fs is os a
    
    data FileStatus = Open | Closed
    
    data File :: FileStatus -> FileStatus -> Type -> Type where
      Open :: FilePath -> File 'Closed 'Open ()
      Close :: FilePath -> File 'Open 'Closed ()
    
    send :: (Inject f i o fs is os) => f i o a -> Eff fs is os a
    
    -- The inferred type would be more general
    openClose :: Eff (File ':> 'Nil) ('Closed ':> 'Nil) ('Closed ':> Nil) ()
    openClose = do
      send (Open "foo.txt")
      send (Close "foo.txt")

  lookup :: Eq a => a -> [(a, b)] -> Maybe b
  lookup _ [] = Nothing
  lookup x ((a, b):abs)
    | a == x = Just b
    | otherwise = lookup x abs

  lookup :: Eq a => a -> [(a, b)] -> b
  lookup x ((a, b):abs)
    | a == x = b
    | otherwise = lookup x abs