Commit cbf3d4b1 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Merge branch 'tc-untouchables'

parents 5010cf35 791f4918
......@@ -2,7 +2,5 @@
annfail05.hs:11:1:
No instance for (Data.Data.Data NoInstances)
arising from an annotation
Possible fix:
add an instance declaration for (Data.Data.Data NoInstances)
In the expression: NoInstances
In the annotation: {-# ANN f NoInstances #-}
......@@ -2,13 +2,10 @@
annfail08.hs:9:1:
No instance for (Data.Data.Data (a0 -> a0))
arising from an annotation
Possible fix:
add an instance declaration for (Data.Data.Data (a0 -> a0))
In the expression: (id + 1)
In the annotation: {-# ANN f (id + 1) #-}
annfail08.hs:9:15:
No instance for (Num (a0 -> a0)) arising from a use of `+'
Possible fix: add an instance declaration for (Num (a0 -> a0))
In the expression: (id + 1)
In the annotation: {-# ANN f (id + 1) #-}
T5380.hs:7:27:
Couldn't match expected type `not_bool' with actual type `Bool'
`not_bool' is a rigid type variable bound by
the type signature for
testB :: not_bool -> (() -> ()) -> () -> not_unit
at T5380.hs:6:10
In the expression: b
In the expression: proc () -> if b then f -< () else f -< ()
In an equation for `testB':
testB b f = proc () -> if b then f -< () else f -< ()
T5380.hs:7:34:
Couldn't match type `not_unit' with `()'
`not_unit' is a rigid type variable bound by
the type signature for
testB :: not_bool -> (() -> ()) -> () -> not_unit
at T5380.hs:6:10
Expected type: () -> not_unit
Actual type: () -> ()
In the expression: f
In the expression: proc () -> if b then f -< () else f -< ()
In an equation for `testB':
testB b f = proc () -> if b then f -< () else f -< ()
T5380.hs:7:27:
Couldn't match expected type `Bool' with actual type `not_bool'
`not_bool' is a rigid type variable bound by
the type signature for
testB :: not_bool -> (() -> ()) -> () -> not_unit
at T5380.hs:6:10
Relevant bindings include
testB :: not_bool -> (() -> ()) -> () -> not_unit
(bound at T5380.hs:7:1)
b :: not_bool (bound at T5380.hs:7:7)
In the expression: b
In the expression: proc () -> if b then f -< () else f -< ()
In an equation for `testB':
testB b f = proc () -> if b then f -< () else f -< ()
T5380.hs:7:34:
Couldn't match type `not_unit' with `()'
`not_unit' is a rigid type variable bound by
the type signature for
testB :: not_bool -> (() -> ()) -> () -> not_unit
at T5380.hs:6:10
Expected type: () -> not_unit
Actual type: () -> ()
Relevant bindings include
testB :: not_bool -> (() -> ()) -> () -> not_unit
(bound at T5380.hs:7:1)
In the expression: f
In the expression: proc () -> if b then f -< () else f -< ()
In an equation for `testB':
testB b f = proc () -> if b then f -< () else f -< ()
arrowfail001.hs:16:36:
No instance for (Foo a)
arising from a use of `foo'
In the expression: foo
In the expression: proc x -> case x of { Bar a -> foo -< a }
In an equation for `get':
get = proc x -> case x of { Bar a -> foo -< a }
arrowfail001.hs:16:36:
No instance for (Foo a) arising from a use of `foo'
In the expression: foo
In the expression: proc x -> case x of { Bar a -> foo -< a }
In an equation for `get':
get = proc x -> case x of { Bar a -> foo -< a }
......@@ -3,7 +3,6 @@ T2851.hs:9:15:
No instance for (Show (F a))
arising from the 'deriving' clause of a data type declaration
Possible fix:
add an instance declaration for (Show (F a))
or use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
When deriving the instance for (Show (D a))
......@@ -3,7 +3,6 @@ T3621.hs:21:21:
No instance for (MonadState state (State s))
arising from the 'deriving' clause of a data type declaration
Possible fix:
add an instance declaration for (MonadState state (State s))
or use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
When deriving the instance for (MonadState state (WrappedState s))
......@@ -4,5 +4,6 @@ class A a oops
data D d = D d
instance A a oops => Read (D a)
data E e = E (D e) deriving Read
instance A Int Bool
......@@ -2,6 +2,10 @@
T5287.hs:6:29:
No instance for (A e oops)
arising from the 'deriving' clause of a data type declaration
The type variable `oops' is ambiguous
Possible fix: add a type signature that fixes these type variable(s)
Note: there is a potential instance available:
instance A Int Bool -- Defined at T5287.hs:7:10
Possible fix:
use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
......
drvfail-foldable-traversable1.hs:9:23:
No instance for (Functor Trivial1)
arising from the 'deriving' clause of a data type declaration
Possible fix:
add an instance declaration for (Functor Trivial1)
or use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
When deriving the instance for (Traversable Trivial1)
drvfail-foldable-traversable1.hs:13:22:
No instance for (Foldable Trivial2)
arising from the 'deriving' clause of a data type declaration
Possible fix:
add an instance declaration for (Foldable Trivial2)
or use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
When deriving the instance for (Traversable Trivial2)
drvfail-foldable-traversable1.hs:17:22:
Can't make a derived instance of `Foldable Infinite':
Constructor `Infinite' must not contain function types
In the data declaration for `Infinite'
drvfail-foldable-traversable1.hs:21:22:
Can't make a derived instance of `Traversable (Cont r)':
Constructor `Cont' must not contain function types
In the data declaration for `Cont'
drvfail-foldable-traversable1.hs:9:23:
No instance for (Functor Trivial1)
arising from the 'deriving' clause of a data type declaration
Possible fix:
use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
When deriving the instance for (Traversable Trivial1)
drvfail-foldable-traversable1.hs:13:22:
No instance for (Foldable Trivial2)
arising from the 'deriving' clause of a data type declaration
Possible fix:
use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
When deriving the instance for (Traversable Trivial2)
drvfail-foldable-traversable1.hs:17:22:
Can't make a derived instance of `Foldable Infinite':
Constructor `Infinite' must not contain function types
In the data declaration for `Infinite'
drvfail-foldable-traversable1.hs:21:22:
Can't make a derived instance of `Traversable (Cont r)':
Constructor `Cont' must not contain function types
In the data declaration for `Cont'
drvfail-functor2.hs:1:29: Warning:
-XDatatypeContexts is deprecated: It was widely considered a misfeature, and has been removed from the Haskell language.
drvfail-functor2.hs:7:14:
Can't make a derived instance of `Functor InFunctionArgument':
Constructor `InFunctionArgument' must not use the type variable in a function argument
In the newtype declaration for `InFunctionArgument'
drvfail-functor2.hs:10:14:
Can't make a derived instance of `Functor OnSecondArg':
Constructor `OnSecondArg' must use the type variable only as the last argument of a data type
In the newtype declaration for `OnSecondArg'
drvfail-functor2.hs:15:14:
Cannot derive well-kinded instance of form `Functor (NoArguments ...)'
Class `Functor' expects an argument of kind `* -> *'
In the newtype declaration for `NoArguments'
drvfail-functor2.hs:20:14:
Can't make a derived instance of `Functor StupidConstraint':
Data type `StupidConstraint' must not have a class context (Eq a)
In the data declaration for `StupidConstraint'
drvfail-functor2.hs:26:14:
No instance for (Functor NoFunctor)
arising from the 'deriving' clause of a data type declaration
Possible fix:
add an instance declaration for (Functor NoFunctor)
or use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
When deriving the instance for (Functor UseNoFunctor)
drvfail-functor2.hs:1:29: Warning:
-XDatatypeContexts is deprecated: It was widely considered a misfeature, and has been removed from the Haskell language.
drvfail-functor2.hs:7:14:
Can't make a derived instance of `Functor InFunctionArgument':
Constructor `InFunctionArgument' must not use the type variable in a function argument
In the newtype declaration for `InFunctionArgument'
drvfail-functor2.hs:10:14:
Can't make a derived instance of `Functor OnSecondArg':
Constructor `OnSecondArg' must use the type variable only as the last argument of a data type
In the newtype declaration for `OnSecondArg'
drvfail-functor2.hs:15:14:
Cannot derive well-kinded instance of form `Functor (NoArguments ...)'
Class `Functor' expects an argument of kind `* -> *'
In the newtype declaration for `NoArguments'
drvfail-functor2.hs:20:14:
Can't make a derived instance of `Functor StupidConstraint':
Data type `StupidConstraint' must not have a class context (Eq a)
In the data declaration for `StupidConstraint'
drvfail-functor2.hs:26:14:
No instance for (Functor NoFunctor)
arising from the 'deriving' clause of a data type declaration
Possible fix:
use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
When deriving the instance for (Functor UseNoFunctor)
......@@ -3,7 +3,6 @@ drvfail001.hs:16:33:
No instance for (Show (f (f a)))
arising from the 'deriving' clause of a data type declaration
Possible fix:
add an instance declaration for (Show (f (f a)))
or use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
When deriving the instance for (Show (SM f a))
......@@ -3,7 +3,6 @@ drvfail002.hs:19:23:
No instance for (X T c)
arising from the 'deriving' clause of a data type declaration
Possible fix:
add an instance declaration for (X T c)
or use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
When deriving the instance for (Show S)
......@@ -3,7 +3,6 @@ drvfail003.hs:16:56:
No instance for (Show (v (v a)))
arising from the 'deriving' clause of a data type declaration
Possible fix:
add an instance declaration for (Show (v (v a)))
or use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
When deriving the instance for (Show (Square_ v w a))
......@@ -3,7 +3,6 @@ drvfail004.hs:8:12:
No instance for (Eq (Foo a b))
arising from the 'deriving' clause of a data type declaration
Possible fix:
add an instance declaration for (Eq (Foo a b))
or use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
When deriving the instance for (Ord (Foo a b))
......@@ -3,7 +3,6 @@ drvfail007.hs:4:38:
No instance for (Eq (Int -> Int))
arising from the 'deriving' clause of a data type declaration
Possible fix:
add an instance declaration for (Eq (Int -> Int))
or use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
When deriving the instance for (Eq Foo)
......@@ -3,7 +3,6 @@ drvfail012.hs:5:33:
No instance for (Eq (Ego a))
arising from the 'deriving' clause of a data type declaration
Possible fix:
add an instance declaration for (Eq (Ego a))
or use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
When deriving the instance for (Ord (Ego a))
......@@ -3,16 +3,14 @@ drvfail013.hs:4:70:
No instance for (Eq (m (Maybe a)))
arising from the 'deriving' clause of a data type declaration
Possible fix:
add an instance declaration for (Eq (m (Maybe a)))
or use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
When deriving the instance for (Eq (MaybeT m a))
drvfail013.hs:6:70:
No instance for (Eq (m (Maybe a)))
arising from the 'deriving' clause of a data type declaration
Possible fix:
add an instance declaration for (Eq (m (Maybe a)))
or use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
When deriving the instance for (Eq (MaybeT' m a))
......@@ -45,7 +45,8 @@ expectedGhcOnlyExtensions = ["ParallelArrays",
"InstanceSigs",
"CApiFFI",
"LambdaCase",
"MultiWayIf"]
"MultiWayIf",
"TypeHoles"]
expectedCabalOnlyExtensions :: [String]
expectedCabalOnlyExtensions = ["Generics",
......
A.hs:6:15:
No instance for (Show (Fields v)) arising from a use of `show'
Possible fix: add an instance declaration for (Show (Fields v))
In the expression: show a
In an equation for `showField': showField a = show a
T3169.hs:13:22:
Could not deduce (Map a ~ MP a b)
from the context (Key a, Key b)
bound by the instance declaration at T3169.hs:10:10-36
Expected type: Map a (Map b elt)
Actual type: Map (a, b) elt
In the second argument of `lookup', namely `m'
In the expression: lookup a m :: Maybe (Map b elt)
In the expression:
case lookup a m :: Maybe (Map b elt) of {
Just (m2 :: Map b elt) -> lookup b m2 :: Maybe elt }
T3169.hs:13:22:
Could not deduce (elt ~ Map b elt)
from the context (Key a, Key b)
......@@ -21,6 +9,11 @@ T3169.hs:13:22:
at T3169.hs:12:3
Expected type: Map a (Map b elt)
Actual type: Map (a, b) elt
Relevant bindings include
lookup :: (a, b) -> Map (a, b) elt -> Maybe elt
(bound at T3169.hs:12:3)
b :: b (bound at T3169.hs:12:13)
m :: Map (a, b) elt (bound at T3169.hs:12:17)
In the second argument of `lookup', namely `m'
In the expression: lookup a m :: Maybe (Map b elt)
In the expression:
......
rw.hs:14:47:
Couldn't match expected type `a' with actual type `Int'
`a' is a rigid type variable bound by
the type signature for writeInt :: T a -> IORef a -> IO ()
at rw.hs:12:12
In the second argument of `writeIORef', namely `(1 :: Int)'
In the expression: writeIORef ref (1 :: Int)
In a case alternative: ~(Li x) -> writeIORef ref (1 :: Int)
rw.hs:19:51:
Couldn't match type `a' with `Bool'
`a' is a rigid type variable bound by
the type signature for readBool :: T a -> IORef a -> IO ()
at rw.hs:16:12
Expected type: a -> Bool
Actual type: Bool -> Bool
In the second argument of `(.)', namely `not'
In the second argument of `(>>=)', namely `(print . not)'
In the expression: readIORef ref >>= (print . not)
rw.hs:14:47:
Couldn't match expected type `a' with actual type `Int'
`a' is a rigid type variable bound by
the type signature for writeInt :: T a -> IORef a -> IO ()
at rw.hs:12:12
Relevant bindings include
writeInt :: T a -> IORef a -> IO () (bound at rw.hs:13:1)
v :: T a (bound at rw.hs:13:10)
ref :: IORef a (bound at rw.hs:13:12)
In the second argument of `writeIORef', namely `(1 :: Int)'
In the expression: writeIORef ref (1 :: Int)
In a case alternative: ~(Li x) -> writeIORef ref (1 :: Int)
rw.hs:19:51:
Couldn't match type `a' with `Bool'
`a' is a rigid type variable bound by
the type signature for readBool :: T a -> IORef a -> IO ()
at rw.hs:16:12
Expected type: a -> Bool
Actual type: Bool -> Bool
Relevant bindings include
readBool :: T a -> IORef a -> IO () (bound at rw.hs:17:1)
v :: T a (bound at rw.hs:17:10)
ref :: IORef a (bound at rw.hs:17:12)
In the second argument of `(.)', namely `not'
In the second argument of `(>>=)', namely `(print . not)'
In the expression: readIORef ref >>= (print . not)
<interactive>:5:1:
No instance for (Show (t -> a)) arising from a use of `print'
Possible fix: add an instance declaration for (Show (t -> a))
In a stmt of an interactive GHCi command: print it
......@@ -3,6 +3,7 @@
No instance for (Show a) arising from a use of `print'
Cannot resolve unknown runtime type `a'
Use :print or :force to determine these types
Relevant bindings include it :: a (bound at <interactive>:6:1)
Note: there are several potential instances:
instance Show Double -- Defined in `GHC.Float'
instance Show Float -- Defined in `GHC.Float'
......@@ -15,6 +16,7 @@
No instance for (Show a) arising from a use of `print'
Cannot resolve unknown runtime type `a'
Use :print or :force to determine these types
Relevant bindings include it :: a (bound at <interactive>:8:1)
Note: there are several potential instances:
instance Show Double -- Defined in `GHC.Float'
instance Show Float -- Defined in `GHC.Float'
......
......@@ -3,6 +3,7 @@
No instance for (Show a1) arising from a use of `print'
Cannot resolve unknown runtime type `a1'
Use :print or :force to determine these types
Relevant bindings include it :: a1 (bound at <interactive>:11:1)
Note: there are several potential instances:
instance Show a => Show (List1 a) -- Defined at ../Test.hs:11:12
instance Show MyInt -- Defined at ../Test.hs:14:16
......
......@@ -12,58 +12,37 @@
In the expression: 'p'
In an equation for `a': a = 'p'
../../typecheck/should_run/Defer01.hs:18:9: Warning:
No instance for (Eq B) arising from a use of `=='
Possible fix: add an instance declaration for (Eq B)
In the expression: x == x
In an equation for `b': b x = x == x
../../typecheck/should_run/Defer01.hs:28:5: Warning:
No instance for (Num (a -> a)) arising from the literal `1'
Possible fix: add an instance declaration for (Num (a -> a))
In the expression: 1
In an equation for `d': d = 1
../../typecheck/should_run/Defer01.hs:25:4: Warning:
Couldn't match type `Int' with `Bool'
Inaccessible code in
a pattern with constructor
C2 :: Bool -> C Bool,
in an equation for `c'
In the pattern: C2 x
In an equation for `c': c (C2 x) = True
../../typecheck/should_run/Defer01.hs:31:5: Warning:
Couldn't match expected type `Char -> t' with actual type `Char'
Relevant bindings include
f :: t (bound at ../../typecheck/should_run/Defer01.hs:31:1)
The function `e' is applied to one argument,
but its type `Char' has none
In the expression: e 'q'
In an equation for `f': f = e 'q'
../../typecheck/should_run/Defer01.hs:34:8: Warning:
Couldn't match expected type `a' with actual type `Char'
`a' is a rigid type variable bound by
the type signature for h :: a -> (Char, Char)
at ../../typecheck/should_run/Defer01.hs:33:6
In the expression: x
In the expression: (x, 'c')
In an equation for `h': h x = (x, 'c')
../../typecheck/should_run/Defer01.hs:39:17: Warning:
Couldn't match expected type `Bool' with actual type `T a'
Relevant bindings include
i :: a -> () (bound at ../../typecheck/should_run/Defer01.hs:39:1)
a :: a (bound at ../../typecheck/should_run/Defer01.hs:39:3)
In the return type of a call of `K'
In the first argument of `not', namely `(K a)'
In the expression: (not (K a))
../../typecheck/should_run/Defer01.hs:43:5: Warning:
No instance for (MyClass a1) arising from a use of `myOp'
In the expression: myOp 23
In an equation for `j': j = myOp 23
../../typecheck/should_run/Defer01.hs:43:10: Warning:
No instance for (Num a1) arising from the literal `23'
The type variable `a1' is ambiguous
Possible fix: add a type signature that fixes these type variable(s)
Note: there are several potential instances:
instance Num Double -- Defined in `GHC.Float'
instance Num Float -- Defined in `GHC.Float'
instance Integral a => Num (GHC.Real.Ratio a)
-- Defined in `GHC.Real'
...plus three others
In the first argument of `myOp', namely `23'
In the expression: myOp 23
In an equation for `j': j = myOp 23
../../typecheck/should_run/Defer01.hs:45:6: Warning:
Couldn't match type `Int' with `Bool'
Inaccessible code in
the type signature for k :: Int ~ Bool => Int -> Bool
../../typecheck/should_run/Defer01.hs:46:7: Warning:
Couldn't match expected type `Bool' with actual type `Int'
......@@ -91,7 +70,6 @@
(deferred type error)
*** Exception: ../../typecheck/should_run/Defer01.hs:18:9:
No instance for (Eq B) arising from a use of `=='
Possible fix: add an instance declaration for (Eq B)
In the expression: x == x
In an equation for `b': b x = x == x
(deferred type error)
......@@ -105,28 +83,36 @@
In the first argument of `print', namely `(c (C2 True))'
*** Exception: ../../typecheck/should_run/Defer01.hs:28:5:
No instance for (Num (a -> a)) arising from the literal `1'
Possible fix: add an instance declaration for (Num (a -> a))
In the expression: 1
In an equation for `d': d = 1
(deferred type error)
*** Exception: ../../typecheck/should_run/Defer01.hs:31:5:
Couldn't match expected type `Char -> t' with actual type `Char'
Relevant bindings include
f :: t (bound at ../../typecheck/should_run/Defer01.hs:31:1)
The function `e' is applied to one argument,
but its type `Char' has none
In the expression: e 'q'
In an equation for `f': f = e 'q'
(deferred type error)
*** Exception: ../../typecheck/should_run/Defer01.hs:34:8:
Couldn't match expected type `a' with actual type `Char'
Couldn't match expected type `Char' with actual type `a'
`a' is a rigid type variable bound by
the type signature for h :: a -> (Char, Char)
at ../../typecheck/should_run/Defer01.hs:33:6
Relevant bindings include
h :: a -> (Char, Char)
(bound at ../../typecheck/should_run/Defer01.hs:34:1)
x :: a (bound at ../../typecheck/should_run/Defer01.hs:34:3)
In the expression: x
In the expression: (x, 'c')
In an equation for `h': h x = (x, 'c')
(deferred type error)
*** Exception: ../../typecheck/should_run/Defer01.hs:39:17:
Couldn't match expected type `Bool' with actual type `T a'
Relevant bindings include
i :: a -> () (bound at ../../typecheck/should_run/Defer01.hs:39:1)
a :: a (bound at ../../typecheck/should_run/Defer01.hs:39:3)
In the return type of a call of `K'
In the first argument of `not', namely `(K a)'
In the expression: (not (K a))
......
<interactive>:6:49:
Couldn't match expected type `a'
with actual type `ListableElem (a, a)'
`a' is a rigid type variable bound by
the instance declaration at <interactive>:6:10
In the expression: a
In the expression: [a, b]
In an equation for `asList': asList (a, b) = [a, b]
<interactive>:6:49:
Couldn't match expected type `a'
with actual type `ListableElem (a, a)'
`a' is a rigid type variable bound by
the instance declaration at <interactive>:6:10
Relevant bindings include
asList :: (a, a) -> [ListableElem (a, a)]
(bound at <interactive>:6:33)
a :: a (bound at <interactive>:6:41)
b :: a (bound at <interactive>:6:43)
In the expression: a
In the expression: [a, b]
In an equation for `asList': asList (a, b) = [a, b]
Simple14.hs:17:12:
Simple14.hs:17:19:
Couldn't match type `z0' with `n'
`z0' is untouchable
inside the constraints (Maybe m ~ Maybe n)
bound at a type expected by the context:
Maybe m ~ Maybe n => EQ_ z0 z0
inside the constraints (Maybe m ~ Maybe n)
bound by a type expected by the context:
Maybe m ~ Maybe n => EQ_ z0 z0
at Simple14.hs:17:12-33
`n' is a rigid type variable bound by
the type signature for foo :: EQ_ (Maybe m) (Maybe n)
at Simple14.hs:16:17
Expected type: EQ_ z0 z0
Actual type: EQ_ m n
Relevant bindings include
foo :: EQ_ (Maybe m) (Maybe n) (bound at Simple14.hs:17:1)
In the second argument of `eqE', namely `(eqI :: EQ_ m n)'
In the first argument of `ntI', namely `(`eqE` (eqI :: EQ_ m n))'
In the expression: ntI (`eqE` (eqI :: EQ_ m n))
......@@ -9,14 +9,25 @@ class SUBST s where
class OBJECT o where
type OTerm o
apply :: (SUBST s, OTerm o ~ STerm s) => s -> o
apply :: (SUBST a, OTerm o ~ STerm a) => a -> o
fce' :: (OTerm a ~ STerm a, OBJECT a, SUBST a) => a -> c
fce' f = fce (apply f)
-- f :: a
-- apply f :: (SUBST a, OBJECT o, OTerm o ~ STerm a) => o
-- fce called with a=o, gives wanted (OTerm o ~ STerm o, OBJECT o, SUBST o)
-- o is a unif var.
fce :: (OTerm o ~ STerm o, OBJECT o, SUBST o) => o -> c
fce f = fce' f