Check a function application isn't possible?

Question

I'd like to check my function signatures mean what I think they mean. I can of course check the positive variants

test_concat : Vect [3] Nat -> Vect [2] Nat -> Vect [5] Nat
test_concat x y = x ++ y

but I'd like to test some negative variants, sth like

test_concat_invalid : Vect [3] Nat -> Vect [2] Nat -> Vect [1] Nat -> Void
test_concat_invalid x y = x ++ y impossible

though obviously the syntax is made up. I've found I can do sth similar to test if I've written a data constructor for proofs correctly. Is this possible?

Answer 1

You can create a type which is indexed by a separate type and value:

data Typed : Type -> a -> Type where
  MkTyped : {A : Type} -> {x : A} -> Typed A x

But only provide a constructor which links the type index with the value index - i.e. Typed can only be constructed if the value x has the type A.

This lets us write a proposition like so:

test_concat_invalid
   : (x : Vect 3 Nat)
  -> (y : Vect 2 Nat) 
  -> Typed (Vect 1 Nat) (x ++ y) 
  -> Void
test_concat_invalid _ _ MkTyped impossible

When Idris tries to unify the types, it sees 1 is not 5 which are obviously different, by construction. This means Idris will happily accept that the MkTyped constructor is impossible in this proposition.