proofsearch003.idr

import Data.Fin

data Wrapper = Wrap (Fin 9)

data Seq : Fin 9 -> Fin 9 -> Type where
  Seq12 : {n : Fin 8} -> Seq (weaken n) (FS n)
  Seq21 : {n : Fin 8} -> Seq (FS n) (weaken n)

interface Evil t where
  value : t -> Fin 9

implementation Evil Wrapper where
  value (Wrap n) = n

consTest : (Evil t) => (a : t) -> (b : t) -> 
           {auto p : Seq (value a) (value b)} -> Bool
consTest _ _ = True

-- Fails!
test1 : Bool
test1 = consTest (Wrap 3) (Wrap 4) -- {p = ?foo}

-- Succeeds!
test2 : Bool
test2 = consTest (Wrap 3) (Wrap 4) {p = Seq12}

-- Succeeds!
test3 : Bool
test3 = consTest (Wrap 3) (Wrap 4) {p = (| Seq12, Seq21 |)}

-- Fails!
-- test4 : Bool
-- test4 = consTest (Wrap 3) (Wrap 4) {p = (| Seq21, Seq12 |)}