Search code examples
implicit-conversionidris

Implicit conversions in Idris 2?

Are implicit conversions still available in Idris 2? This Idris 1 code

data Foo : Type -> Type where
  MkFoo : t -> Foo t

public export implicit
IntFoo : Int -> Foo Int
IntFoo = MkFoo

now fails to compile in Idris 2 with

Error: Parse error at line 95:1:
Couldn't parse declaration (next
tokens: [public, export, implicit, identifier IntFoo, symbol :, identifier Int, symbol ->, identifier Foo, identifier Int, identifier IntFoo])

Moving implicit doesn't fix it, and it compiles fine if I remove implicit.

Btw I looked in the docs for updating from 1 to 2 but can't see anything about this. If you know where to look, a link would also be nice.

Solution

  • Implicit conversions are not supported in Idris 2. I believe their exclusion is deliberate.