Resolving ambiguous type variable

I have a term type, which in essence is:

data Term a = Term a Bool
            deriving Show

The Bool is kind of a helper, and is only occasionally needed. I'd like the user to be able to skip it if it isn't necessary. Meaning the following should work:

main :: IO ()
main = print v
 where v = "a"
         =: Term "b" True
         =: []

where:

class Join a b where
   (=:) :: a -> [b] -> [b]
   infixr 1 =:

instance Join a (Term a) where
   x =: y = Term x False : y

instance Join (Term a) (Term a) where
   x =: y = x : y

Alas, GHC complains:

a.hs:15:8-12: error: [GHC-39999]
    • Ambiguous type variable ‘b0’ arising from a use of ‘print’
      prevents the constraint ‘(Show b0)’ from being solved.
      Relevant bindings include v :: [b0] (bound at a.hs:17:8)

But if I write main like this:

main :: IO ()
main = print v
 where v :: [Term String]
       v = "a"
         =: Term "b" True
         =: []

Then all is well. (Note the only difference is I gave v a type signature.)

I'm curious if there's a modern GHC trick (Type-families, Injective-Type-families, Closed-type-families, GADTs, etc., or some magic flags) that would make the type signature unnecessary and let GHC deduce the type itself without any help.

Here's the program in its entirety:

data Term a = Term a Bool
            deriving Show

class Join a b where
   (=:) :: a -> [b] -> [b]
   infixr 1 =:

instance Join a (Term a) where
   x =: y = Term x False : y

instance Join (Term a) (Term a) where
   x =: y = x : y

main :: IO ()
main = print v
 where v :: [Term String]  -- Want to avoid this signature and let GHC deduce it.
       v = "a"
         =: Term "b" True
         =: []

And the question is if there's some GHC feature or trick I can apply so the type-signature on v is not necessary. I'm also happy to change the Join class or add new parameters/dependencies etc., so long as the local definition of v can be written as is without the type signature.

I'd also appreciate an explanation of why this wouldn't be possible, if there's a good legitimate reason why what I'm asking for is unreasonable. It seems to me like there's enough type-info around for GHC to deduce the type itself, but I suspect some sort of "open-world" assumption is kicking in and none of the "closed-type-family" like tricks won't work; if that is indeed the case. To be clear, I'm perfectly happy for the Join class to never be instantiated at any other type.

Solution

Here's one approach. You can use a closed type family that selects the correct right-hand side type based on the left-hand side type:

type family Terms a where
  Terms (Term a) = [Term a]
  Terms a = [Term a]

and define the =: operator as a plain polymorphic function using this family:

infixr 1 =:
(=:) :: a -> Terms a -> Terms a
(=:) = undefined

Now, your main compiles because the left-hand side of each =: call forces an unambiguous right-hand side type:

main :: IO ()
main = print v
 where v = "a"
         =: Term "b" True
         =: []

Of course, (=:) = undefined is a decidedly suboptimal implementation. To implement =: properly, you'll need to use a constraint to dispatch to the correct definition:

(=:) :: (Join a (Terms a)) => a -> Terms a -> Terms a
(=:) = join

With appropriate class and instance definitions:

class Join a b where
  join :: a -> b -> b

instance Join a [Term a] where
  join x y = Term x False : y

instance Join (Term a) [Term a] where
  join x y = x : y

the complete program seems to work as intended:

{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE TypeFamilies #-}

data Term a = Term a Bool
  deriving (Show)

type family Terms a where
  Terms (Term a) = [Term a]
  Terms a = [Term a]

class Join a b where
  join :: a -> b -> b

instance Join a [Term a] where
  join x y = Term x False : y

instance Join (Term a) [Term a] where
  join x y = x : y

infixr 1 =:
(=:) :: (Join a (Terms a)) => a -> Terms a -> Terms a
(=:) = join

main :: IO ()
main = print v
  where v =  "a"
          =: Term "b" True
          =: []