example.idr

module Example

interface Base (f : x -> Type) where
  base : (x -> Type) -> x -> Type

interface Base f => Corecursive (f : x -> Type) where
  cbase : (x -> Type) -> x -> Type
  cbase {f} = base {f}

-- When checking right hand side of Example.default#cbase with expected type
--         (x ->
--         Type) ->
--         x ->
--         Type
-- 
-- Can't find implementation for Base f
-- 
-- Possible cause:
--         example.idr:8:24:When checking argument f to function Example.base:
--                 Type mismatch between
--                         x1 ->
--                         Type (Type of f)
--                 and
--                         x ->
--                         Type (Expected type)
--                 
--                 Specifically:
--                         Type mismatch between
--                                 x1
--                         and
--                                 x