跟踪约束的技术

Question

这是一个场景：我编写了一些带有类型签名的代码，而GHC抱怨无法推导出某些x和y的x~y。您通常可以给GHC一个骨头，简单地将同构添加到函数约束中，但这是一个坏主意，原因有几个：

null

{-# LANGUAGE GADTs, FlexibleContexts, TypeOperators #-}
import Data.Syntactic

-- Based on NanoFeldspar.hs
data Let a where
    Let :: Let (a :-> (a -> b) :-> Full b)

share :: (Let :<: sup,
          Domain a ~ sup,
          Domain b ~ sup,
          SyntacticN (a -> (a -> b) -> b) fi) 
      => a -> (a -> b) -> a
share = sugarSym Let

null

Answer 1

你在GHC 8.8+中尝试过吗？

share :: (Let :<: sup,
          Domain a ~ sup,
          Domain b ~ sup,
          SyntacticN (a -> (a -> b) -> b) fi,
          _) 
      => a -> (a -> b) -> a
share = sugarSym Let

关键是在约束中使用类型洞:_=>your donald type