Gleb Alexeyev (5) [Avatar] Offline
[ 151 bytes ]
[ 449 bytes ]
Hello again!
I'm struggling with exercise 2 from section 10.3.4 which reads as follows: 'Define a view which allows other modules to inspect the abstract data type'.

The definition is pretty obvious, but I'm getting an error about inaccessible pattern variables.
-- file Shape.idr
module Shape

export data Shape = Rectangle Double Double | Circle Double

rectangle : Double -> Double -> Shape
rectangle = Rectangle

circle : Double -> Shape
circle = Circle

public export
data ShapeView : Shape -> Type where
  SRectangle : ShapeView (rectangle a b)
  SCircle : ShapeView (circle r)

total shapeView : (shape: Shape) -> (ShapeView shape)
shapeView (Rectangle a b) = SRectangle
shapeView (Circle r) = SCircle

-- file ex10_3_4.idr
import Shape

area : Shape -> Double
area shape with (shapeView shape)
  area (rectangle a b) | SRectangle = a * b
  area (circle r) | SCircle = r * r

Error message:
Type checking ./Shape.idr
Type checking ./ex10_3_4.idr
ex10_3_4.idr:5:3:b is not an accessible pattern variable
Holes: Main.area

I downloaded the code for the book as well to see if I made some stupid mistake, but the code for this particular exercise (see file Chapter10/Exercises/ex_10_3_4.idr) is defined in 1 module, breaking it in 2 modules produces the same compiler error.

I'm using idris version 0.99.1 built with stack for Mac OS X.
Edwin Brady (65) [Avatar] Offline
Oh dear, sorry about this. This turns out to be caused by an error introduced by an optimisation in the typechecker which I implemented a couple of months ago. I'm glad you caught it!

I've fixed it in master, so in the next release (and therefore 1.0) it'll work fine.
Gleb Alexeyev (5) [Avatar] Offline
Thanks, Edwin, the fix was really fast!