Idris-dev icon indicating copy to clipboard operation
Idris-dev copied to clipboard

Can't find implementation

Open nicolabotta opened this issue 4 years ago • 0 comments

The program

> import Data.List

> %default total
> %auto_implicits off
> %access public export

> NaturalTransformation : {F, G : Type -> Type} -> 
>                         (Functor F, Functor G) => 
>                         ({T : Type} -> F T -> G T) -> Type
>                         
> NaturalTransformation {F} h = {X, Y : Type} -> (f : X -> Y) -> (fx : F X) -> 
>                               (map f . h) fx = (h . map f) fx                         

> listToMaybe_NaturalTransformation : NaturalTransformation {F = List} {G = Maybe} listToMaybe
> listToMaybe_NaturalTransformation f  Nil      = Refl
> listToMaybe_NaturalTransformation f (x :: xs) = Refl

> using (F : Type -> Type)
>   implementation [FunctorComposition] Functor F => Functor (F . F) where
>     map = map . map  

> using implementation FunctorComposition
>   joinNaturalTransformation : NaturalTransformation {F = List . List} {G = List} join

fails to type check with

- + Errors (1)
 `-- ./Monad/issue.lidr line 23 col 30:
     When checking type of Main.joinNaturalTransformation:
     Can't find implementation for Functor (List . List)

Is this the expected behavior? How can one state that join for lists is a natural transformation in Idris?

nicolabotta avatar Dec 14 '19 15:12 nicolabotta