Internal Error: Proof done

[barakmich]

Steps to Reproduce

Minimal code snippet reproduces:

module ListProof

import Prelude.List
import Prelude.Nat
import Prelude.Bool

placeSorted' : (n : Nat) -> (l : List Nat) -> List Nat
placeSorted' n [] = [n]
placeSorted' n (x :: xs) =
  if (n <= x) then (n :: x :: xs) else (x :: (placeSorted' n xs))

total
cutH : (x : Nat) -> (ys : List Nat) -> sorted (x :: ys) = True -> sorted ys = True
cutH x [] prf = Refl
cutH x (y :: xs) prf with (x <= y)
  cutH x (y :: xs) prf | True = prf
  cutH x (y :: xs) prf | False = absurd prf

psProof : (x : Nat) -> (xs : List Nat) -> sorted xs = True -> sorted (placeSorted' x xs) = True
psProof x [] y = Refl
psProof x (z :: zs) y with (x <= z) proof p
  psProof x (z :: zs) y | True = rewrite y in rewrite sym p in Refl
  psProof x (z :: zs) y | False = let ih = psProof x zs (cutH z zs y) in rewrite sym y in ?t

Expected Behavior

Type check on ?t to finish the proof

Observed Behavior

When checking right hand side of with block in ListProof.psProof with expected type
        sorted (if False then x :: z :: zs else z :: placeSorted' x zs) = True

INTERNAL ERROR: Proof done, nothing to run tactic on: Solve
<snip>
This is probably a bug, or a missing error message.
Please consider reporting at https://github.com/idris-lang/Idris-dev/issues

[michaelmesser]

I have a similar issue https://github.com/idris-lang/Idris-dev/issues/4217

[ahmadsalim]

Thanks for reporting the issue. This does seem like a weird bug indeed.

As a workaround, consider using replace explicitly instead of rewrite.

[barakmich]

Out of curiosity, what would that workaround look like?

[ahmadsalim]

I don't know the concrete type, but usually you can replace rewrite p in e with replace {P = \x => t x} p e

[ahmadsalim]

i.e., see type of replace:

replace : (x = y) -> P x -> P y
    Perform substitution in a term according to some equality.