No such variable imp

[treeowl]

Well, it's true, there is no such variable that I know of.

module CopumpkinStyleFingerTrees

import Prelude.Algebra
import Classes.Verified

-- %default total

data Digit : Type -> Type where
  One   : a -> Digit a
  Two   : a -> a -> Digit a
  Three : a -> a -> a -> Digit a
  Four  : a -> a -> a -> a -> Digit a

measureDigit : Semigroup v => (a -> v) -> Digit a -> v
measureDigit f (One   a)       = f a
measureDigit f (Two   a b)     = f a <+> f b
measureDigit f (Three a b c)   = f a <+> f b <+> f c
measureDigit f (Four  a b c d) = f a <+> f b <+> f c <+> f d

mapDigit : (a -> b) -> Digit a -> Digit b
mapDigit f (One   a)       = One   (f a)
mapDigit f (Two   a b)     = Two   (f a) (f b)
mapDigit f (Three a b c)   = Three (f a) (f b) (f c)
mapDigit f (Four  a b c d) = Four  (f a) (f b) (f c) (f d)

data Node : (v : Type) -> (a : Type) -> (f : a -> v) -> Type where
  Node2 : Monoid v => (m : v) -> (x : a) -> (y : a)            -> (pf : m = f x <+> f y)         -> Node v a f
  Node3 : Monoid v => (m : v) -> (x : a) -> (y : a) -> (z : a) -> (pf : m = f x <+> f y <+> f z) -> Node v a f

measureNode : Monoid v => Node v a f -> v
measureNode (Node2 m _ _ _)   = m
measureNode (Node3 m _ _ _ _) = m

mapNode : Monoid w => (a -> b) -> (g : b -> w) -> Node v a f -> Node w b g
mapNode f g (Node2 m a b   pf) = Node2 _ (f a) (f b)       Refl
mapNode f g (Node3 m a b c pf) = Node3 _ (f a) (f b) (f c) Refl

mutual
  data FingerTree : (v : Type) -> (a : Type) -> (f : a -> v) -> Type where
    Empty  : FingerTree v a f
    Single : a -> FingerTree v a f
    Deep   : Monoid v => (m : v) -> (left : Digit a) -> (child : FingerTree v (Node v a f) measureNode) -> (right : Digit a) -> (pf : m = measureDigit f left <+> measureTree child <+> measureDigit f right) -> FingerTree v a f

  measureTree : Monoid v => FingerTree v a f -> v
  measureTree Empty = neutral
  measureTree {f} (Single a) = f a
  measureTree (Deep m l c r pf) = m

mapTree : Monoid w => (a -> b) -> (g : b -> w) -> FingerTree v a f -> FingerTree w b g
mapTree f g Empty = Empty
mapTree f g (Single a) = Single (f a)
mapTree f g (Deep m l c r pf) = Deep _ (mapDigit f l) (mapTree (mapNode f g) measureNode c) (mapDigit f r) Refl

--  mapTreePreserve : Monoid v => (m : a -> b) -> (g : b -> v) -> (req : {x : a} -> g (m x) = f x) -> FingerTree v a f -> FingerTree v b g
--mapTreePreserve m g req Empty = Empty
--mapTreePreserve m g req (Single a) = Single (m a)
--mapTreePreserve m g req (Deep s pr mid sf prf) = ?tttt

mutual
  mapTreePreserve : Monoid v => (f : a -> b) -> (mb : b -> v) -> (req : {x : a} -> mb (f x) = ma x) -> FingerTree v a ma -> FingerTree v b mb
  mapTreePreserve f g r Empty = Empty
  mapTreePreserve f g r (Single a) = Single (f a)
  mapTreePreserve f g r (Deep m pr mid sf pf) =
    let pr' = mapDigit f pr
        mid' = mapTreePreserve (mapNode f g) measureNode ?prf mid
        sf' = mapDigit f sf
    in ?mapTreePreserve_rhs

  lm : Monoid v => (t : FingerTree v a ma) -> measureTree (mapTreePreserve f mb r t) = measureTree t
  lm Empty = Refl
  lm (Single a) = ?lmsing
  lm (Deep m l c r pf) = ?lmdeep

[david-christiansen]

This is almost certainly a failure to solve an implicit argument in some nested context. It's an atrocious error message.

Turning on logging yields this monstrosity:

Monoid v => (t : FingerTree v a ma) -> measureTree (mapTreePreserve f mb r t) = measureTree t
Elaborated: pat {a522} : Type 0. (v : Type 0) -> (a : Type 0) -> (ma : a -> v) -> (f : a -> {a522}) -> (mb : {a522} -> v) -> (r : = v v (mb (f {imp0})) (ma {imp0})) -> ({constrarg0} : Prelude.Algebra.Monoid v) -> (t : CopumpkinStyleFingerTrees.FingerTree v a ma) -> = v v (CopumpkinStyleFingerTrees.measureTree v {a522} mb {constrarg0} (CopumpkinStyleFingerTrees.mapTreePreserve v a {a522} ma {constrarg0} f mb (\ {imp0} : a => r) t)) (CopumpkinStyleFingerTrees.measureTree v a ma {constrarg0} t)

Glagh! I don't get why it's pattern-binding {a522}.

[edwinb]

The real error here is that it can't infer the type of 'r' in lm. The "imp" is the name of an implicit lambda - I am going to change this so that it at least gets the name from the implicit argument - but that imp ends up in the type of 'r' which can't be put in a sensible place in the type, hence the "No such variable" error.

There does seem to be an error in lm which you can find out by making more of its types explicit, but I can probably find a way for it to say "Couldn't infer a type for r" or some such instead of the unhelpful No Such Variable error.

[treeowl]

Yes, I strongly suspect the previous "less-than-helpful error message" tag was actually the right thing to have on this. A certain amount of abstraction leakage may be inherent in a language with implicits, but there are some boundaries that shouldn't be crossed. No, I don't know how to define such, nor how to allow for improved error messages at the boundaries. As @edwinb has stated, implicits seem to be a rather dark art.