Yes, and that functional language is LISP, as demonstrated by the parentheses and Cons operator, and a few other things I probably didn't catch. I suppose it's less educational, and more just a meta-level trolling.
Cons is not exclusively a Lisp operation, Haskell's lists (among other languages) are implemented with cons: [1,2] is syntactic sugar for 1:2:(). And the parens are also part of the Haskell syntax, not something added to make it look like Lisp - note the lack of parens around the outermost types.
If anything it seems closest to Idris, given the Peano arithmetic...
I don't think it's actually Lisp. Lisp is essentially an imperative language; you use functional concepts, but you're telling the computer what concrete thing to do at each step. This is just asking it to resolve types in a type system, using whatever algorithm it likes to satisfy the type constraints.
Note, in particular, the complete lack of algorithm to solve the actual n-queens problem: just the constraints.
Fair enough, I pretty much nope'd out after the "Haskell is a dynamically-typed, interpreted language" bit, scrolled to the end, and saw some LISP-y output.
If anything it seems closest to Idris, given the Peano arithmetic...