Eric B (4) [Avatar] Offline
Pasting the exercise's code here for convenience:

area : Shape -> Double
area s with (shapeView s)
  area (triangle base height) | STriangle = ?area_rhs_1
  area (rectangle width height) | SRectangle = ?area_rhs_2
  area (circle radius) | SCircle = ?area_rhs_3

After defining a ShapeView (and covering function shapeView), Idris yells at me when I try to load the file with the area skeleton above:

- + Errors (1)
 `-- Shape.idr line 40 col 7:
     When checking left hand side of with block in Shape.area:
     Can't match on with block in Shape.area (triangle base height) STriangle

If I capitalize the shape names in the patterns (so as to match on their constructors instead of the exported functions) and fill in the right-hand sides:

??> :total area
Shape.area is possibly not total due to:
    with block in Shape.area, which is not total as there are missing cases

Are there typos in the book? Should we be matching on the data constructors instead?

How can I prove to Idris that area is total?

Please advise.
Edwin Brady (65) [Avatar] Offline
Hi Eric,
Sorry for the slow reply, I've been travelling (and writing smilie).

In my solution to this exercise, area is total. What's your definition of 'shapeView'? The code in the book looks fine, and the same as the code in my solution. Perhaps you could paste your entire file and I'll take a look.
Eric B (4) [Avatar] Offline
Thanks for the reply, Edwin. I've just taken another look and fixed it. Can't wait for v11!