How can I turn a [TExp a] into a TExp [a], or otherwise apply refineTH to multiple values programatically?

I've been using refined for refinement types in Haskell recently, and have encountered a major usability problem. I can't figure out how to refine an entire list of values at compile time.

For example I can write:

{-# LANGUAGE TemplateHaskell #-}

import Refined

oneToThree :: [Refined Positive Int]
oneToThree = [$$(refineTH 1), $$(refineTH 2), $$(refineTH 3)]

But I can't do this precludes the ability of using range syntax, because Refined doesn't (for good reason) have an instance for Enum.

I would like to be able to do something like

oneToThree :: [Refined Positive Int]
oneToThree = $$(traverse refineTH [1..3])

but I can't get this to compile because I can't lift [TExp (Refined Positive Int)] into TExp [Refined Positive Int].

Is there template haskell magic that I missing that will let me do this?

Would also be open to suggestions for better lightweight refinement type libraries if someone has a suggestion.

sequenceQTExpList :: [Q (TExp a)] -> Q (TExp [a])
sequenceQTExpList [] = [|| [] ||]
sequenceQTExpList (x:xs) = [|| $$(x) : $$(sequenceQTExpList xs) ||]

Then use it as

$$(sequenceQTExpList $ map refineTH [1..3])

You're right that it feels like a traverse. The type is a bit off, though, with the extra Qs floating around. I don't see anything offhand that lets you combine those layers usefully.

Unfortunately, a lot of the mechanism used there is TH syntax rather than functions. There just isn't an obvious way to do both the lifting and the splicing as functions, so you're stuck writing bespoke helpers for each container type instead of getting to use Traversable. It's an interesting problem. If there's a clean solution, it'd have a good chance of making it into a future version of template Haskell if it was brought up to the maintainers. But I just don't see it right now.