我知道在设计模块化Haskell代码时，可以使用newtypes来避免泄漏抽象。实际上，这是我遇到的使用newtypes与类型同义词（和懒惰？）之间唯一讨论的区别。然而，我注意到当被别名化的类型是 * 多态和受约束 * 时，行为上的一些令人惊讶的差异。
请考虑以下示例：

{-# 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))

字符串
我还没有完全弄清楚细节，但我相信HOAS sem将sem :: [Type] -> Type -> Type描述为某种形式的 * 单调 predicate 相对单子 *（相对于Var sem）。
现在你可以看到，我们可以编写像ex这样的程序，其中变量在不同的上下文中使用，Haskell正确地计算出了约束条件。实际上，在使用站点，变量的环境被计算出是外部项之一，唯一出现的约束条件是env ≤ env的形式，因此是不连贯的示例。
This definition of HOAS enables me to write a total and completely safe conversion to well-scoped (co-) de Bruijn syntax of STLC。这证实了使sem相对于Var sem仍然排除了外来项。

但是，即使我们不需要弱化变量，我们在使用变量的时候还是要给它们加上前缀ret，这有点不幸。

但是，如果我将Var的定义更改为只是一个类型同义词，Haskell就不再高兴了。

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)

型
考虑到上面的变化（我只是删除了Var的构造函数，类型签名保持不变），我的示例不再进行类型检查，并且我得到了关于重叠示例的错误日志，例如：
·由于使用“z”而引起的env“≤ env”2的重叠示例
现在看起来，当一个类型同义词是多态的约束时，约束在 bind 站点示例化，而不是在use站点示例化。这是正确的吗？这是预期的吗？这有文档记录吗？
Agda中的等效示例（使用Var作为常规别名）工作正常，因为毫无疑问，环境（隐式参数）在使用站点上是统一的：

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)

型