Skip to content

Cannot define recursive bound on associated type of an interface #4917

@casper-pragma

Description

@casper-pragma

I have a need to define something like the following:

interface A T => A a where
  T : Type

I have tried it with version 1.3.4 and it says it does not see T in scope.

Can I define it in idris?


If I were to define it in haskell, I would go like so:

class A (T b) => A b where
  type T b :: *

Need an equivalent in idris tho :3

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions