Using constraints in Typed Template Haskell

Question

I would like to use typeclass constraints in my Typed Template Haskell snippets, but just can't get them to work: the instances seem to be missing inside the splice.

Here is a standalone, minimized version of my code to demonstrate the issue. The first module defines a Typed Template Haskell macro memoryMap which doesn't impose any constraints on tag, and ram0, which constrains tag by C:

{-# LANGUAGE TemplateHaskell, QuasiQuotes #-}
{-# LANGUAGE DerivingStrategies, GeneralizedNewtypeDeriving #-}
module RetroClash.MemoryTH where

import Control.Monad.Identity
import Language.Haskell.TH

class C a where

newtype Signal tag a = Signal{ runSignal :: a }

newtype Addressing dom a = Addressing
    { runAddressing :: Identity a
    }
    deriving newtype (Functor, Applicative, Monad)

memoryMap :: Addressing tag () -> TExpQ (Signal tag (Maybe dat) -> Signal tag (Maybe dat))
memoryMap addressing = [|| \ wr -> wr ||]

ram0 :: (C tag) => Addressing tag ()
ram0 = pure ()

Then I try to use it in a straightforward way from another module:

{-# LANGUAGE TemplateHaskell #-}
module RetroClash.MemoryTHTest where

import RetroClash.MemoryTH

foo
    :: (C tag)
    => Signal tag (Maybe Int)
    -> Signal tag (Maybe Int)
foo = $$(memoryMap ram0)

However, this results in the following type error from GHC 8.10:

src/RetroClash/MemoryTHTest.hs:11:20: error:
    • No instance for (C tag) arising from a use of ‘ram0’
    • In the first argument of ‘memoryMap’, namely ‘ram0’
      In the expression: memoryMap ram0
      In the Template Haskell splice $$(memoryMap ram0)
   |
11 | foo = $$(memoryMap ram0)
   |                    ^^^^

One thing I've tried just for the heck of it is to add the C constraint to the macro's return type directly:

memoryMap :: Addressing tag () -> TExpQ (C tag => Signal tag (Maybe dat) -> Signal tag (Maybe dat))
memoryMap addressing = [|| \ wr -> wr ||]

Even if this worked, it wouldn't solve my original problem, because the constraints should come, in an open-world way, from whatever happens in the Addressing tag () argument; but anyway this version fails because it runs into GHC's impredicativity limitations:

    • Illegal qualified type:
        C tag => Signal tag (Maybe dat) -> Signal tag (Maybe dat)
      GHC doesn't yet support impredicative polymorphism

Packer

Answer 1

This unfortunately is a fundamental flaw of the current implementation of Typed Template Haskell, with no easy workaround available.

Constraints are simply not handled correctly.

We've been running into the same problem when looking at how to implement a staged version of generics-sop. You might want to have a look at Section 5 of the Staged Sums of Products paper. We also have a solution for the handling of constraints in Template Haskell, but this solution needs implementation in GHC, and that at the moment is only available in an experimental branch (see the staged-sop repo for some instructions on how to try it). At the moment, the branch is in limbo, because is needs significant rebasing due to all the linear types changes. Hopefully, we get around to doing that at some point soon, because I would really like to have proper constraint handling in Typed Template Haskell.

Undetermined