相关疑难解决方法(0)

我最近发布了一个问题,关于句法2.0有关的定义share.我在GHC 7.6中有这个工作:

{-# LANGUAGE GADTs, TypeOperators, FlexibleContexts #-}

import Data.Syntactic
import Data.Syntactic.Sugar.BindingT

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

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

但是,GHC 7.8希望-XAllowAmbiguousTypes …

这是我的代码:

{-# LANGUAGE TypeFamilies, TypeOperators, DataKinds, PolyKinds, FlexibleContexts, UndecidableInstances #-}

module Foo where

import Data.Singletons.Prelude
import Data.Type.Equality

data TP a b

-- foldl (\(bool, r) x -> (bool && (r == x), r)) (True, head xs) xs
type family Same (b :: Bool) (r :: k) (rq :: [k]) :: k where
  Same bool r (x ': xs) = Same (bool :&& (r == x)) r xs
  Same bool r '[] = TP bool r

data NotEqualFailure
-- converts a …