-XIncoherentInstances doesn't work

Question

I've been messing around with the syntactic library (version 2.0 on github), and I have a small example that causes GHC(i) 7.6.2 to complain about IncoherentInstances.

{-# LANGUAGE FlexibleInstances, 
TypeFamilies,
TypeOperators,
OverlappingInstances, 
UndecidableInstances,
GADTs,
FlexibleContexts,
IncoherentInstances #-}

import Data.Syntactic
import Data.Syntactic.Functional

type family FunToAST (dom :: * -> *) f
type instance FunToAST dom (Full a) = ASTF dom a
type instance FunToAST dom (a :-> fi) = ASTF dom a -> FunToAST dom fi

data Let a where
    Let :: Let (a :-> (a -> b) :-> Full b)

share :: (Let :<: dom,
          ApplySym sig fi dom, 
          SyntacticN (Denotation sig) fi, 
          fi ~ FunToAST dom sig)
          => Denotation sig
share = sugarSym Let

Fine. I'm not asking why I need IncoherentInstances. The problem is, when I include that extension, I get the exact same error message:

Overlapping instances for SyntacticN
                            (Denotation sig)
                            (ASTF sup0 a0 -> ASTF sup0 (a0 -> b0) -> 
                            ASTF sup0 b0)
  arising from a use of `sugarSym'
Matching instances:
  instance [overlap ok] (Syntactic f, Domain f ~ sym,
                         fi ~ AST sym (Full (Internal f))) =>
                        SyntacticN f fi
    -- Defined in `Data.Syntactic.Sugar'
  instance [overlap ok] (Syntactic a, Domain a ~ sym,
                         ia ~ Internal a, SyntacticN f fi) =>
                        SyntacticN (a -> f) (AST sym (Full ia) -> fi)
    -- Defined in `Data.Syntactic.Sugar'
(The choice depends on the instantiation of `sig, sup0, a0, b0'
 To pick the first instance above, use -XIncoherentInstances
 when compiling the other instance declarations)
In the expression: sugarSym Let
In an equation for `share2': share2 = sugarSym Let

I doubt this problem is actually related to the library, but I don't know enough about IncoherentInstances to write my own example.