Shadowed definitions cause ask to reject its own suggestions

[dunhamsteve]

I got into a confusing loop where ask was rejecting a line that it had previously suggested. In the following code, ask will repeatedly add "I don't see why you need this", because it intends the + in the proposal to be the first one and is reading it back as the second one. Consider not allowing shadowing of names in definitions.

data Number = Z | S Number

(+) :: Number -> Number -> Number
defined x + y inductively x where
  defined x + y from x where
    defined Z + y = y
    defined S x + y = S (x + y)

prop AddOn Number Number where
  prove AddOn a c by Adding b where
   prove a + b = c

(+) :: Number -> Number -> Number
defined x + y inductively x where
  defined x + y from x where
    defined Z + y = y
    defined S x + y = S (x + y)


prove AddOn a b -> AddOn b c -> AddOn a c by ImpI where
   given AddOn a b prove AddOn b c -> AddOn a c from AddOn a b where
     {- I don't see why you need this
     given a + b = b prove AddOn b c -> AddOn a c ?
     -}
     {- I don't see why you need this
     given a + x252 = b prove AddOn b c -> AddOn a c ?
     -}
     given a + x254 = b prove AddOn b c -> AddOn a c ?

I see that there was a line of code to prevent re-declarations, but I presume it was commented out for a reason:

ask/lib/Language/Ask/ChkRaw.hs

Line 739 in 51ee4b6

-- cope (what's f) (\ gr -> return ()) (\ _ -> gripe $ AlreadyDeclared f)

Uncommenting that line resolves the issue, but it looks like ask still allows re-defining (+), which could be sketchy if you write proofs about (+) and then change its definition.