The Author Online Book Forums are Moving

The Author Online Book Forums will soon redirect to Manning's liveBook and liveVideo. All book forum content will migrate to liveBook's discussion forum and all video forum content will migrate to liveVideo. Log in to liveBook or liveVideo with your Manning credentials to join the discussion!

Thank you for your engagement in the AoF over the years! We look forward to offering you a more enhanced forum experience.

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 (66) [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!