Difference between newtypes and type synonyms for polymorphic constrained types

Question

I know that newtypes can be used to avoid leaky abstractions when designing modular Haskell code. It's actually the only discussed difference between using newtypes versus type synonyms that I've encountered (and laziness?). However I'm noticing some surprising difference in behavior when the type being aliased is polymorphic and constrained.

Consider the following example:

{-# LANGUAGE DataKinds, GADTs, BlockArguments, UnicodeSyntax #-}
module Main where

import Data.Kind (Type, Constraint)

-- a class for type environment extension
infix 4 ≤
type (≤) :: [Type] -> [Type] -> Constraint
class xs ≤ ys where

instance {-# INCOHERENT #-}  xs ≤ ys
instance {-# INCOHERENT #-} '[] ≤ ys
instance xs ≤ ys =>   xs ≤ a:ys
instance xs ≤ ys => a:xs ≤ a:ys

---

-- finally, tagless HOAS for stlc with let-bindings
type HOAS :: ([Type] -> Type -> Type) -> Constraint
class HOAS sem where

  lam   :: (∀ env'. env ≤ env' => Var sem env' a -> sem env' b)
        -> sem env (a -> b)

  app   :: sem env (a -> b) -> (sem env a -> sem env b)

  -- a flipped version of the let binding
  flet  :: (∀ env'. env ≤ env' => Var sem env' a -> sem env' b)
        -> (sem env a -> sem env b)

-- regular let binding
let_ :: HOAS sem
     => sem env a -> (∀ env'. env ≤ env' => Var sem env' a -> sem env' b)
     -> sem env b
let_ x f = flet f x

ret :: Var sem env a -> (∀ env'. env ≤ env' => sem env' a)
ret (V x) = x

type Var :: ([Type] -> Type -> Type) -> ([Type] -> Type -> Type)
newtype Var sem env a = V (∀ env'. env ≤ env' => sem env' a)

---

ex :: forall sem. HOAS sem => sem '[] (Bool -> Bool)
ex =
  let_ (lam \z -> ret z) (\z ->
    app (lam \x -> app (ret x) (ret z))
        (lam \y -> ret z))

I haven't worked out the details fully yet, but I believe HOAS sem characterises sem :: [Type] -> Type -> Type as some form of monotonous predicate relative monad (relative over Var sem).

Now you can see that we can write programs like ex where variables are used in different contexts, and Haskell figures out the constraints properly. Indeed, at use site, the environment of variables is figured out to be the one of the outer term, and the only constraints that arise are of the form env ≤ env hence the incoherent instance.

This definition of HOAS enables me to write a total and completely safe conversion to well-scoped (co-) de Bruijn syntax of STLC. Which confirms that making sem relative to Var sem still rules out exotic terms.

But, even though we don't have to weaken variables, we still have to prefix them with ret when using them, which is a bit unfortunate.

However, if I change the definition of Var to just a type synonym, Haskell is no longer happy.

ret :: Var sem env a -> (∀ env'. env ≤ env' => sem env' a)
ret x = x

type Var :: ([Type] -> Type -> Type) -> ([Type] -> Type -> Type)
type Var sem env a = (∀ env'. env ≤ env' => sem env' a)

Considering the changes above (where I literally just remove the constructor for Var, type signatures remain the same), my example no longer type-checks, and I get a log of errors about overlapping instances such as:

• Overlapping instances for env' ≤ env'2 arising from a use of ‘z’

Now it looks like when a type synonym is polymorphic with a constraint, the constraint gets instanciated at bind site, rather than at use site. Is this correct? Is this expected? Is this documented somewhere?

The equivalent example in Agda (with Var a regular alias) works fine, because there is no doubt the environment (implicit argument) is unified at the use site:

open import Agda.Builtin.List
open import Agda.Builtin.Bool

private variable
  a b               : Set
  xs ys zs env env' : List Set

infix 4 _≤_
data _≤_ : (xs ys : List Set) → Set₁ where
  base : [] ≤ ys
  keep : xs ≤ ys → a ∷ xs ≤ a ∷ ys
  drop : xs ≤ ys →     xs ≤ a ∷ ys

instance
  ≤-refl : ∀ {xs} → xs ≤ xs
  ≤-refl {xs = []    } = base
  ≤-refl {xs = x ∷ xs} = keep ≤-refl

Sem : Set₂
Sem = List Set → Set → Set₁

Var : Sem → Sem
Var sem env a = ∀ {env'} → ⦃ env ≤ env' ⦄ → sem env' a

record HOAS (sem : List Set → Set → Set₁) : Set₂ where
  field
    lam'  : (∀ {env'} → ⦃ env ≤ env' ⦄ → Var sem env' a → sem env' b)
          → sem env (a → b)

    app'  : sem env (a → b) → (sem env a → sem env b)

    let' : sem env a
         → (∀ {env'} → ⦃ env ≤ env' ⦄ → Var sem env' a → sem env' b)
         → sem env b

  infix -1 let' lam'
  syntax let' a (λ x → b) = let[ x ← a ] b
  syntax lam' (λ x → b)   = ƛ[ x ] b
  syntax app' f x = f $ x

open HOAS ⦃...⦄

ex : ∀ {sem} → ⦃ HOAS sem ⦄ → sem [] (Bool -> Bool)
ex = let[ z ← ƛ[ x ] x ] (ƛ[ x ] x $ z) $ (ƛ[ y ] z)

Answer 1

I actually figured it out right after submitting. The issue is GADTs implies MonoLocalBind, which no longer generalizes local binds (which I assume applies to function arguments). If I explicitly set NoMonoLocalBind, Var can now be defined as a regular type synonym, no syntactic noise, all is good!