Interaction of constraints and top-level splices is poorly specified and hard to control

On a fresh Thursday morning I set out to achieve the seemingly simple task of defining an instance for a type using typed template haskell. However, as I am sure the reader can already guess, I ran into some unexpected difficulties concerning type class constraints.

Code: https://github.com/mpickering/tth-define-instances

Take 1

I want to implement an Ord instance using the generically defined gcompare. gcompare requires each field of the datatype to be an instance of Ord, as it is recursive, including the instance we are currently defining.

instance Ord (BinTree Int) where                                                
    compare = $$(gcompare)  

gcompare_1 :: (GenericSyntax a, All (All Ord) (Description a)) => Q (TExp (a -> a -> Ordering)))

However, this leads to an error because we can't use the instance for Ord (BinTree Int) in the top-level splice, because it's being define in the current module, it would be possible to use it to influence the code we are currently generating.

Use.hs:14:16: error:
    • GHC stage restriction:
        instance for ‘Ord
                        (BinTree
                           Int)’ is used in a top-level splice, quasi-quote, or annotation,
        and must be imported, not defined locally
    • In the expression: gcompare
      In the Template Haskell splice $$(gcompare)
      In the expression: $$(gcompare)
   |
14 |   compare = $$(gcompare)
   |       

The problem is, the use of the Ord dictionary is in fact safe, because it's only used in generated code.

In order to reflect the static information about the dictionaries, I modified the definition of gcompare in order to explicitly take the necessary evidence.

Take 2

gcompare_2 :: GenericSyntax a => POP Compa (Description a) -> Syntax (a -> a -> Ordering)

data Compa a where                                                              
   Compa :: Q (TExp (a -> a -> Ordering)) -> Compa a  

gcompare_2 takes an explicit argument which plays the role of the All (All Ord) xs constraint from gcompare_1 but with the difference that we only have access to the comparison functions in the next stage.

This means we can use gcompare_2 as follows:

Attempt 1

Firstly just trying to use it directly in the instance with quoted compare functions. I expected this to work.

instance Ord (BinTree Int) where                                                
    compare = $$(gcompare_2 (POP (Nil :* ((Compa [|| compare ||] :* Compa [|| compare ||] :* Compa [|| compare ||] :* Nil) :* Nil))))

Use.hs:21:48-62: error:
    • GHC stage restriction:
        instance for ‘Ord
                        (BinTree
                           Int)’ is used in a top-level splice, quasi-quote, or annotation,
        and must be imported, not defined locally
    • In the Template Haskell quotation [|| compare ||]
      In the first argument of ‘Compa’, namely ‘[|| compare ||]’
      In the first argument of ‘(:*)’, namely ‘Compa [|| compare ||]’
   |
21 |   compare = $$(gcompare_2 (POP (Nil :* ((Compa [|| compare ||] :* Compa [|| compare ||] :* Compa 
[|| compare ||] :* Nil) :* Nil))))
   |                                                ^^^^^^^^^^^^^^^

Analysis: GHC isn't smart enough to know that compare is the function we are currently defining.

Attempt 2

Try defining the function just at the top-level without the complications of the instance.

compareBinTree :: (Ord a) => BinTree a -> BinTree a -> Ordering                       
compareBinTree = $$(gcompare_2 (POP (Nil :* ((Compa [|| compareBinTree ||] :* Compa [|| compare ||] :* Compa [|| compareBinTree ||] :* Nil) :* Nil))))

Still doesn't work.

Use.hs:25:53-74: error:
    • No instance for (Ord a) arising from a use of ‘compareBinTree’
    • In the Template Haskell quotation [|| compareBinTree ||]
      In the first argument of ‘Compa’, namely ‘[|| compareBinTree ||]’
      In the first argument of ‘(:*)’, namely
        ‘Compa [|| compareBinTree ||]’
   |
25 | compareBinTree = $$(gcompare_2 (POP (Nil :* ((Compa [|| compareBinTree ||] :* Compa [|| compare ||] 
:* Compa [|| compareBinTree ||] :* Nil) :* Nil))))
   |                                                     ^^^^^^^^^^^^^^^^^^^^^^

Analysis: This looks like a simple bug of the constraint environment not being restored inside a quotation.

Attempt 3

Explicitly pass the comparison argument, this one works.

compareBinTree :: (a -> a -> Ordering) -> BinTree a -> BinTree a -> Ordering    
compareBinTree c = $$(gcompare_2 (POP (Nil :* ((Compa [|| compareBinTree c ||] :* Compa [|| c ||] :* Compa [|| compareBinTree c ||] :* Nil) :* Nil))))
                                                                                                   
instance Ord (BinTree Int) where                                                
    compare = compareBinTree compare  

---

It's not clear what to do about this ticket. It's clear that generating code which relies on constraints is currently quite inconvenient.

cc @kosmikus