TH doesn't work with ambiguous constraints

[isovector]

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TemplateHaskell     #-}

module Sem.IPFS where

import Polysemy
import Lang
import Types

data IPFS m a where
  GetIpfs :: LanguageAdapter l => Hash -> IPFS m (Maybe (AST l))
  PutIpfs :: LanguageAdapter l => AST l -> IPFS m ()

makeSem ''IPFS

given

class LanguageAdapter l where
  type AST l

produces the error:

/home/sandy/prj/ngs/src/Sem/IPFS.hs:14:1: error:                                             
    • Could not deduce: AST l ~ AST l0                                                       
      from the context: (Polysemy.Internal.Union.MemberWithError IPFS r,                     
                         LanguageAdapter l)                                                  
        bound by the type signature for:                                                     
                   putIpfs :: forall k (r :: [Effect]) (l :: k).                             
                              (Polysemy.Internal.Union.MemberWithError IPFS r,
                               LanguageAdapter l) =>
                              AST l -> Sem r ()
        at /home/sandy/prj/ngs/src/Sem/IPFS.hs:14:1-14
      NB: ‘AST’ is a non-injective type family 
      The type variable ‘l0’ is ambiguous
    • In the first argument of ‘PutIpfs’, namely ‘x_ad4w’
      In the first argument of ‘Polysemy.Internal.send’, namely
        ‘(PutIpfs x_ad4w :: IPFS (Sem r_ad4v) ())’
      In the expression:
        Polysemy.Internal.send (PutIpfs x_ad4w :: IPFS (Sem r_ad4v) ())
    • Relevant bindings include
        x_ad4w :: AST l (bound at /home/sandy/prj/ngs/src/Sem/IPFS.hs:14:1)
        putIpfs :: AST l -> Sem r ()
          (bound at /home/sandy/prj/ngs/src/Sem/IPFS.hs:14:1)
   |
14 | makeSem ''IPFS
   | ^^^

@TheMatten do you know offhand why this happens? I'm actually surprised by the behavior here.

[isovector]

(it works just fine if AST is an assocated data fam)

[TheMatten]

Hmm, isn't it basically what GHC says? AST is non-injective, thus it can't infer l from it's type - data family works simply because it is injective.

[TheMatten]

This example shows that we can't fill in type of action completely just using final annotation - we may consider switching to TypeApplications instead.

[isovector]

I was reasonably sure we type apply everything anyway, in order to get around the ambiguous types?

[isovector]

oh right -- we just produce a final type sig. yeah, that makes sense