向实例添加约束时的奇怪行为

Question

我正在使用语法库来处理AST.我有一些奇怪的行为,我不是正在发生的事情.

{-# LANGUAGE TypeOperators, GADTs, FlexibleInstances,
    FlexibleContexts, UndecidableInstances #-}
module Foo where

import Data.Syntactic
import Data.Syntactic.Functional

data Const a where Const :: Const (Full a)
instance Render Const where renderSym Const = "const"

main :: ASTF Const Int
main = foo $ inj Const

class Foo dom where
  foo :: ASTF dom a -> ASTF dom a

instance --(Const :<: dom) => 
    Foo dom where
  foo node | Just Const <- prj node = error "PASS"
  foo _ = error "FAIL"

bar :: (Const :<: dom) => ASTF dom a -> ASTF dom a
bar node | Just Const <- prj node = error "PASS"
bar _ = error "FAIL"

问题1

我可以在没有约束的Foo情况下定义一个实例Const :<: dom,但是我不知道有没有任何方法可以在bar没有该约束的情况下进行编译(GHC建议IncoherentInstances如果我保留约束bar).什么是不同的bar,foo这允许我不使用约束foo？

问题2

虽然我可以在Foo没有约束的情况下定义实例,但在main上面的代码中运行会打印"FAIL".但是,如果我Const :<: dom在实例中添加(取消注释)约束,则main打印"PASS".什么Haskell机器可以添加不必要的约束并改变行为？在这个例子中具体发生了什么导致这种行为？我怀疑它可能与Syntactic库中的重叠/不可判断/不连贯的实例有关.(注意:bar始终打印"PASS".)