Unsolved metavariable for function that has no inhabited arguments

Question

I am getting an unsolved metavariable for foo in the code below:

namespace Funs
  data Funs : Type -> Type where
    Nil : Funs a
    (::) : {b : Type} -> (a -> List b) -> Funs (List a) -> Funs (List a)

  data FunPtr : Funs a -> Type -> Type where
    here : FunPtr ((::) {b} _ bs) b
    there : FunPtr bs b -> FunPtr (_ :: bs) b

total foo : FunPtr [] b -> Void

How do I convince Idris that foo has no valid patterns to match on?

I've tried adding

foo f = ?foo

and then doing a case split in Emacs on f (just to see what might come up), but that just removes the line, leaving foo as an unsolved meta.

Answer 1

It turns out all I need to do is enumerate all possible patterns for foo's argument, and then Idris is able to figure out, one by one, that they are un-unifyable with foo's type:

foo : FunPtr [] b -> Void
foo here impossible
foo (there _) impossible