Bind not strictly positive

[justjoheinz]

This snippet is taken from idris-free (https://github.com/idris-hackers/idris-free) which does not compile currently. This issue is about the error messages the compilation produces, not about the fact that Free does not compile:

data Free : (f : Type -> Type) -> (a : Type) -> Type where
  Pure : a -> Free f a
  Bind : f (Free f a) -> Free f a

instance Functor f => Functor (Free f) where
  map f (Pure x) = Pure (f x)
  map f (Bind x) = assert_total (Bind (map (map f) x))

The first error message one gets is :

Prelude.Functor.Control.Monad.Free.Free f implementation of Prelude.Functor.Functor, 
method map is possibly not total due to: Control.Monad.Free.Bind

Inspecting the docs of map gives the standard map function of the Functor interface which declares map to be total. This left me puzzled, because I was not able to get the totality state of this map implementation.

I then inspected the docs for Free

Data type Control.Monad.Free.Free : (f : Type -> Type) -> (a : Type) -> Type
    
    
Constructors:
    Pure : a -> Free f a
        
        
    Bind : f (Free f a) -> Free f a

(nothing unusual here) and finally Bind. The docs for Bind say:

Control.Monad.Free.Suspend : f (Free f a) -> Free f a
    
    
    The function is not strictly positive

I tried to find out what "strictly positive" means. Some Adga and Coq resources later (which I am not fluent with), there seems to be a problem that Free occurs on the left hand side of the constructor arrow. Again I am puzzled - why does

(::) : a -> List a -> List a 

work as a constructor for List then?

As a user of Idris, I would like that

• Idris reports that map is not total because Bind is not strictly positive
• Idris explains a bit better what exactly being strictly positive entitles
• as a bonus: that Idris provides error messages which link to an error message wiki page on Github, giving more detailed information about the nature of the error.

[justjoheinz]

D'oh - I opened this issue on idris-free, it was meant to go to Idris itself. I copy it there.

[clayrat]

Here's the link to that issue idris-lang/Idris-dev#3752

[clayrat]

https://personal.cis.strath.ac.uk/fredrik.nordvall-forsberg/talks/AIMXXV/variantsIR.pdf seems to describe a way to encode strictly positive inductive types