diff --git a/NominalAngluin.cabal b/NominalAngluin.cabal
index 9ba936b..a81a303 100644
--- a/NominalAngluin.cabal
+++ b/NominalAngluin.cabal
@@ -20,11 +20,13 @@ executable NominalAngluin
     Examples.Stack,
     NLStar,
     ObservationTable,
-    Teacher
+    Teacher,
+    Teachers.Teacher,
+    Teachers.Terminal,
+    Teachers.Whitebox
   build-depends:
     base >= 4.8 && < 5,
     containers,
-    deepseq,
     haskeline,
     mtl,
     NLambda >= 1.1
diff --git a/src/AbstractLStar.hs b/src/AbstractLStar.hs
index 12df888..d72368b 100644
--- a/src/AbstractLStar.hs
+++ b/src/AbstractLStar.hs
@@ -4,7 +4,6 @@ module AbstractLStar where
 import ObservationTable
 import Teacher
 
-import Control.DeepSeq (deepseq)
 import Debug.Trace
 import NLambda
 
@@ -48,7 +47,6 @@ learn :: LearnableAlphabet i
   -> State i
   -> Automaton (BRow i) i
 learn makeComplete handleCounterExample constructHypothesis teacher s =
-    deepseq s $ -- This helps ordering the traces somewhat.
     trace "##################" $
     trace "1. Making it complete and consistent" $
     let s2 = makeComplete teacher s in
diff --git a/src/Examples/Contrived.hs b/src/Examples/Contrived.hs
index 8f152ce..9f117d4 100644
--- a/src/Examples/Contrived.hs
+++ b/src/Examples/Contrived.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeriveGeneric, DeriveAnyClass #-}
 module Examples.Contrived where
 
 import           NLambda
@@ -12,8 +12,8 @@ import           GHC.Generics (Generic)
 -- Example automaton from the whiteboard. Three orbits with 0, 1 and 2
 -- registers. The third orbit has a local symmetry (S2).
 data Example1 = Initial | S1 Atom | S2 (Atom, Atom)
-  deriving (Show, Eq, Ord, Generic)
-instance BareNominalType Example1
+  deriving (Show, Eq, Ord, Generic, NominalType, Contextual)
+
 example1 :: Automaton Example1 Atom
 example1 = automaton
     -- states, 4 orbits (of which one unreachable)
@@ -36,8 +36,9 @@ example1 = automaton
 
 -- Accepts all even words (ignores the alphabet). Two orbits, with a
 -- trivial action. No registers.
-data Aut2 = Even | Odd deriving (Eq, Ord, Show, Generic)
-instance BareNominalType Aut2
+data Aut2 = Even | Odd
+  deriving (Eq, Ord, Show, Generic, NominalType, Contextual)
+
 example2 :: Automaton Aut2 Atom
 example2 = automaton
     -- states, two orbits
@@ -55,8 +56,9 @@ example2 = automaton
 
 -- Accepts all non-empty words with the same symbol. Three orbits: the initial
 -- state, a state with a register and a sink state.
-data Aut3 = Empty | Stored Atom | Sink deriving (Eq, Ord, Show, Generic)
-instance BareNominalType Aut3
+data Aut3 = Empty | Stored Atom | Sink
+  deriving (Eq, Ord, Show, Generic, NominalType, Contextual)
+
 example3 :: Automaton Aut3 Atom
 example3 = automaton
     -- states, three orbits
@@ -84,8 +86,8 @@ data Aut4 = Aut4Init              -- Initial state
           | Second Atom Atom      -- After reading two different symbols
           | Symm Atom Atom Atom   -- Accepting state with C3 symmetry
           | Sorted Atom Atom Atom -- State without symmetry
-  deriving (Eq, Ord, Show, Generic)
-instance BareNominalType Aut4
+  deriving (Eq, Ord, Show, Generic, NominalType, Contextual)
+
 example4 :: Automaton Aut4 Atom
 example4 = automaton
     -- states
@@ -123,8 +125,8 @@ example4 = automaton
 
 -- Accepts all two-symbols words with different atoms
 data Aut5 = Aut5Init | Aut5Store Atom | Aut5T | Aut5F
-    deriving (Eq, Ord, Show, Generic)
-instance BareNominalType Aut5
+    deriving (Eq, Ord, Show, Generic, NominalType, Contextual)
+
 example5 :: Automaton Aut5 Atom
 example5 = automaton
     -- states
diff --git a/src/Examples/ContrivedNFAs.hs b/src/Examples/ContrivedNFAs.hs
index c444095..ff3b0f8 100644
--- a/src/Examples/ContrivedNFAs.hs
+++ b/src/Examples/ContrivedNFAs.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeriveGeneric, DeriveAnyClass #-}
 {-# LANGUAGE TupleSections #-}
 module Examples.ContrivedNFAs where
 
@@ -14,8 +14,8 @@ import           GHC.Generics (Generic)
 -- The complement of 'all distinct atoms'
 -- Not determinizable
 data NFA1 = Initial1 | Guessed1 Atom | Final1
-  deriving (Show, Eq, Ord, Generic)
-instance BareNominalType NFA1
+  deriving (Show, Eq, Ord, Generic, NominalType, Contextual)
+
 exampleNFA1 :: Automaton NFA1 Atom
 exampleNFA1 = automaton
     -- states, 4 orbits (of which one unreachable)
@@ -43,8 +43,8 @@ exampleNFA1 = automaton
 -- So this one *is* determinizable.
 -- Also used in the Bollig et al paper.
 data NFA2 = Initial2 | Distinguished Atom | Count Int
-  deriving (Show, Eq, Ord, Generic)
-instance BareNominalType NFA2
+  deriving (Show, Eq, Ord, Generic, NominalType, Contextual)
+
 exampleNFA2 n = automaton
     (singleton Initial2
         `union` map Distinguished atoms
diff --git a/src/Examples/Fifo.hs b/src/Examples/Fifo.hs
index 0e308d0..bc00ff0 100644
--- a/src/Examples/Fifo.hs
+++ b/src/Examples/Fifo.hs
@@ -1,7 +1,6 @@
 {-# LANGUAGE DeriveGeneric, DeriveAnyClass #-}
 module Examples.Fifo (DataInput(..), fifoExample) where
 
-import Control.DeepSeq (NFData)
 import           GHC.Generics (Generic)
 import           NLambda
 import           Prelude      (Eq, Int, Maybe (..), Ord, Show, Read, length, reverse,
@@ -12,7 +11,8 @@ import qualified Prelude      ()
 -- Functional queue data type. First list is for push stuff onto, the
 -- second list is to pop. If the second list is empty, it will reverse
 -- the first.
-data Fifo a = Fifo [a] [a] deriving (Eq, Ord, Show, Generic)
+data Fifo a = Fifo [a] [a]
+  deriving (Eq, Ord, Show, Generic, NominalType, Contextual)
 
 push :: a -> Fifo a -> Fifo a
 push x (Fifo l1 l2) = Fifo (x:l1) l2
@@ -35,16 +35,12 @@ sizeFifo (Fifo l1 l2) = length l1 + length l2
 -- nominal automaton.
 
 -- The alphabet:
-data DataInput = Put Atom | Get Atom deriving (Eq, Ord, Show, Read, Generic, NFData)
-instance BareNominalType DataInput
-instance Contextual DataInput where
-    when f (Put a) = Put (when f a)
-    when f (Get a) = Get (when f a)
+data DataInput = Put Atom | Get Atom
+  deriving (Eq, Ord, Show, Read, Generic, NominalType, Contextual)
 
 -- The automaton: States consist of fifo queues and a sink state.
 -- This representation is not minimal at all, but that's OK, since the
 -- learner will learn a minimal anyways. The parameter n is the bound.
-instance BareNominalType a => BareNominalType (Fifo a)
 fifoExample :: Int -> Automaton (Maybe (Fifo Atom)) DataInput
 fifoExample n = automaton
     -- states
diff --git a/src/Examples/RunningExample.hs b/src/Examples/RunningExample.hs
index 59b2158..3dd8f4d 100644
--- a/src/Examples/RunningExample.hs
+++ b/src/Examples/RunningExample.hs
@@ -19,7 +19,7 @@ import           GHC.Generics (Generic)
 
 -- Parametric in the alphabet, because why not?
 data RunningExample a = Store [a] | Check [a] | Accept | Reject
-  deriving (Eq, Ord, Show, Generic, BareNominalType)
+  deriving (Eq, Ord, Show, Generic, NominalType, Contextual)
 
 runningExample alphabet 0 = automaton
     (fromList [Accept, Reject])
diff --git a/src/Examples/Stack.hs b/src/Examples/Stack.hs
index a472f81..185ef15 100644
--- a/src/Examples/Stack.hs
+++ b/src/Examples/Stack.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeriveGeneric, DeriveAnyClass #-}
 module Examples.Stack (DataInput(..), stackExample) where
 
 import           Examples.Fifo (DataInput (..))
@@ -10,7 +10,8 @@ import qualified Prelude       ()
 
 
 -- Functional stack data type is simply a list.
-data Stack a = Stack [a] deriving (Eq, Ord, Show, Generic)
+data Stack a = Stack [a]
+  deriving (Eq, Ord, Show, Generic, NominalType, Contextual)
 
 push :: a -> Stack a -> Stack a
 push x (Stack l1) = Stack (x:l1)
@@ -35,7 +36,6 @@ sizeStack (Stack l1) = length l1
 
 -- The automaton: States consist of stacks and a sink state.
 -- The parameter n is the bound.
-instance BareNominalType a => BareNominalType (Stack a)
 stackExample :: Int -> Automaton (Maybe (Stack Atom)) DataInput
 stackExample n = automaton
     -- states
diff --git a/src/ObservationTable.hs b/src/ObservationTable.hs
index 7b6a795..0e6512b 100644
--- a/src/ObservationTable.hs
+++ b/src/ObservationTable.hs
@@ -10,7 +10,6 @@ module ObservationTable where
 import           NLambda      hiding (fromJust)
 import           Teacher
 
-import           Control.DeepSeq (NFData, force)
 import           Data.Maybe   (fromJust)
 import           Debug.Trace  (trace)
 import           GHC.Generics (Generic)
@@ -43,7 +42,7 @@ type Row i o = Fun [i] o
 
 -- This is a rather arbitrary set of constraints
 -- But I use them *everywhere*, so let's define them once and for all.
-type LearnableAlphabet i = (NFData i, Contextual i, NominalType i, Show i)
+type LearnableAlphabet i = (Contextual i, NominalType i, Show i)
 
 -- `row is` denotes the data of a single row
 -- that is, the function E -> O
@@ -83,17 +82,7 @@ data State i = State
     , ee  :: Set [i]  -- suffixes
     , aa  :: Set i    -- alphabet (remains constant)
     }
-    deriving (Show, Ord, Eq, Generic, NFData, BareNominalType)
-
-instance NominalType i => Conditional (State i) where
-    cond f s1 s2 = fromTup (cond f (toTup s1) (toTup s2)) where
-        toTup State{..} = (t,ss,ssa,ee,aa)
-        fromTup (t,ss,ssa,ee,aa) = State{..}
-
-instance (Ord i, Contextual i) => Contextual (State i) where
-    when f s = fromTup (when f (toTup s)) where
-        toTup State{..} = (t,ss,ssa,ee,aa)
-        fromTup (t,ss,ssa,ee,aa) = State{..}
+    deriving (Show, Ord, Eq, Generic, NominalType, Conditional, Contextual)
 
 -- Precondition: the set together with the current rows is prefix closed
 addRows :: LearnableAlphabet i => Teacher i -> Set [i] -> State i -> State i