Possible Idris compiler bug

Example.idr

module Example

import Data.Nat.DivMod

nextBlockSize : Nat -> Nat
nextBlockSize k with (divMod k 511)
  nextBlockSize (remainder + (quotient * 512)) | (MkDivMod quotient remainder remainderSmall) = ?nextBlockSize_rhs_1

Example2.idr

-- this time with explicit "the Nat 512"
module Example

import Data.Nat.DivMod

nextBlockSize : Nat -> Nat
nextBlockSize k with (divMod k 511)
  nextBlockSize (remainder + (quotient * (the Nat 512))) | (MkDivMod quotient remainder remainderSmall) = ?nextBlockSize_rhs_1

output.txt

*/tmp/Example> :r
Type checking /tmp/Example.idr
/tmp/Example.idr:7:40-41:When checking left hand side of with block in Example.nextBlockSize:
When checking an application of function Prelude.Interfaces.*:
        Type mismatch between
                Integer (Type of 512)
        and
                Nat (Expected type)
Holes: Example.nextBlockSize

output2.txt

*/tmp/Example> :r
Type checking /tmp/Example.idr
/tmp/Example.idr:7:17:When checking left hand side of with block in Example.nextBlockSize:
Type mismatch between
        remainder + quotient * 512 (Inferred value)
and
        remainder + quotient * the Nat 512 (Given value)

Specifically:
        Type mismatch between
                plus
        and
                (+)
Holes: Example.nextBlockSize