Haskell typeclass constraint cannot be resolved due to Paterson's conditions

Question

I'm trying to build an AST with indexed nested annotations. I added a typeclass for peeling the annotation at the top-level and tried to provide default instances that effectively says "if you know how to peel an annotation on its own, then you know how to peel an annotation at the particular AST node."

Since one of my tree nodes is a Nat indexed Predicate and its parent existentially quantifies this variable, when I try to write the instance for the parent, I get stuck at Paterson's conditions. Namely, I have more type variables in my assertion than I do in the head.

If I turn on UndecidableInstances, then GHC cannot unify the variables with kind Nat.

If I further turn on AllowAmbiguousTypes, then I get a more absurd error where it says it cannot find an instance despite the fact that the instance it is looking for is in the assertion of the type instance.

My questions are:

1. Is this actually a bad instance to write, or is the type checker too conservative?
2. If it is bad or there is no way around the problem, how else can I provide this default peeling behaviour?

Here's minimalish code (I stripped the bits not essential to the type error, so some bits might seem redundant):

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

module Constraint where

data AnnType = ABase

data family PredicateAnn (a :: AnnType)
data instance PredicateAnn (a :: AnnType) = PABase

data Nat = Zero | Succ Nat

data Predicate (n :: Nat) (a :: AnnType) = Predicate
data Literal   (a :: AnnType) = forall n. Literal (Predicate n a)

class PeelableAST (ast :: AnnType -> *) (ann :: AnnType -> AnnType) where
  peel :: ast (ann a) -> ast a

class PeelableAnn (f :: AnnType -> *) (ann :: AnnType -> AnnType) where
  peelA :: f (ann a) -> f a

instance PeelableAST (Predicate n) ann
         => PeelableAST Literal ann where
  peel (Literal predicate) = Literal (peel predicate)

instance PeelableAnn PredicateAnn ann => PeelableAST (Predicate n) ann where
  peel Predicate = Predicate

Here's the exact error without UndecidableInstances:

src/Constraint.hs:27:10: error:
• Variable ‘n’ occurs more often
    in the constraint ‘PeelableAST (Predicate n) ann’
    than in the instance head
  (Use UndecidableInstances to permit this)
• In the instance declaration for ‘PeelableAST Literal ann’
   |
27 | instance PeelableAST (Predicate n) ann
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

And here's the one with it:

src/Constraint.hs:28:10: error:
• Could not deduce (PeelableAST (Predicate n0) ann)
  from the context: PeelableAST (Predicate n) ann
    bound by an instance declaration:
               forall (n :: Nat) (ann :: AnnType -> AnnType).
               PeelableAST (Predicate n) ann =>
               PeelableAST Literal ann
    at src/Constraint.hs:(28,10)-(29,35)
  The type variable ‘n0’ is ambiguous
• In the ambiguity check for an instance declaration
  To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
  In the instance declaration for ‘PeelableAST Literal ann’
   |
28 | instance PeelableAST (Predicate n) ann
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

Here is the one with AllowAmbiguousTypes:

 src/Constraint.hs:31:39: error:
• Could not deduce (PeelableAnn PredicateAnn ann)
    arising from a use of ‘peel’
  from the context: PeelableAST (Predicate n) ann
    bound by the instance declaration
    at src/Constraint.hs:(29,10)-(30,35)
• In the first argument of ‘Literal’, namely ‘(peel predicate)’
  In the expression: Literal (peel predicate)
  In an equation for ‘peel’:
      peel (Literal predicate) = Literal (peel predicate)
   |
31 |   peel (Literal predicate) = Literal (peel predicate)
   |                                       ^^^^^^^^^^^^^^

EDIT:

As Daniel Wagner suggests one solution is to make PeelableAnn PredicateAnn ann an assertion in PeelableAST Literal ann instance. However, I never use peelA defined by PeelableAnn in PeelableAST Literal ann definition and I'd like this instance to behave as the default behaviour and be able to overwrite it by directly providing a PeelableAST (Predicate n) ann instance. In other words, peeling might be inherently contextual.

Since PeelableAnn PredicateAnn ann is required by PeelableAST (Predicate n) ann, I feel that GHC should be able to find and satisfy this condition.

I can simply have a bogus PeelableAnn PredicateAnn ann instance only to be ignored by the more specific one, but that is quite hacky

Answer 1

In your PeelableAST Literal ann instance, you use the PeelableAST (Predicate n) ann instance. If the type-checker wants to use that instance, it must verify its precondition, namely, that PeelableAnn PredicateAnn ann holds. But it doesn't know this, because you have not made it a precondition of your PeelableAST Literal ann instance.

That's okay; it's easy to fix, and lets you avoid an ambiguous type entirely. Just add the precondition it's worried about as a precondition for you PeelableAST Literal ann instance. Indeed, since it's now the precondition for both instances, you can then also drop the PeelableAnn PredicateAnn ann precondition, as it's implied by this new and stronger condition. So:

instance PeelableAnn PredicateAnn ann => PeelableAST Literal ann where
    peel (Literal predicate) = Literal (peel predicate)

You can then delete AllowAmbiguousTypes, though UndecidableInstances is still needed because PeelableAnn PredicateAnn ann is not obviously structurally smaller than PeelableAST Literal ann.