我正在使用抽象语法树，我想给 Binders 提供他们自己的类型 . 这似乎给伊德里斯的整体检查带来了问题......
有一个典型的自我参照 Tree 伊德里斯完全检查完成 .
data TreeShape = Last | More TreeShape TreeShape
Show TreeShape where
show Last = "Leaf"
show (More left right) = "Branch " ++ show left ++ " " ++ show right
同样有一个相互 Tree ：
mutual
data MuTree = Another MuMuTree
data MuMuTree = TheLeaf | TheBranch MuTree MuMuTree
Show MuTree where
show (Another x) = show x
Show MuMuTree where
show TheLeaf = "Leaf"
show (TheBranch left right) = "Branch " ++ show left ++ " " ++ show right
但是，通过对提取的类型进行参数化来引入间接，并且总体检查失败：
data LeftBranch t = L t
(Show t) => Show (LeftBranch t) where
show (L x) = show x
data TreeOutline = Final | Split (LeftBranch TreeOutline) TreeOutline
Show TreeOutline where
show Final = "Leaf"
show (Split left right) = "Branch " ++ show left ++ " " ++ show right
有没有办法让Idris正确检查最后一种递归类型的总体？除此之外，除了使用 assert_total s代码之外还有什么东西吗？