Hi,
When I read the book, I tried answering exercise 2 from section 10.3.4 in the spirit of section 10.3, which is to hide implementation details.
So I kept file Shape_abs.idr as described in the book, and added a ShapeView and associated covering function (with export modifiers):
module Shape_abs
export
data Shape = Triangle Double Double
 Rectangle Double Double
 Circle Double
export
triangle : Double > Double > Shape
triangle = Triangle
export
rectangle : Double > Double > Shape
rectangle = Rectangle
export
circle : Double > Shape
circle = Circle
public export
data ShapeView : Shape > Type where
STriangle : ShapeView (triangle base height)
SRectangle : ShapeView (rectangle width height)
SCircle : ShapeView (circle radius)
export
shapeView : (input : Shape) > ShapeView input
shapeView (Triangle x y) = STriangle
shapeView (Rectangle x y) = SRectangle
shapeView (Circle x) = SCircle
and then, in the exercise file (ex10_3_4.idr), I wrote (using the usual TypeDefineRefine process) :
import Shape_abs
area : Shape > Double
area s with (shapeView s)
area (triangle base height)  STriangle = ?area_rhs_rhs_1
area (rectangle width height)  SRectangle = ?area_rhs_rhs_2
area (circle radius)  SCircle = ?area_rhs_rhs_3
However, at this stage, I got a typechecking error : "height is not an accessible pattern variable", and couldn't proceed further.
I saw your solution, which was to define the area function straight after defining the view, but how can I use the view from another module?
Thank you for the wonderful book
Martin
