[Added a generator for type pairs, of which the right one is more general.
tobias@goedderz.info**20150326174238
 Ignore-this: d8bb9b79eeb6f81db275dae9994715da
 
 This is useful for testing "match", which should succeed iff its right argument
 is more general.
] 
<
[Added a Size instance for Type
tobias@goedderz.info**20150326091807
 Ignore-this: d7dad3b1c30bd379d860d0adbc6f6bcb
] 
> hunk ./src/Tests.hs 9
+import Data.List (mapAccumL, nubBy)
hunk ./src/Tests.hs 14
+import qualified Control.Monad.State as St
hunk ./src/Tests.hs 63
+newtype MatchingTypes = MatchingTypes { getMatchingTypes :: (Type, Type) }
+    deriving Show
+
+instance QC.Arbitrary MatchingTypes where
+    arbitrary = do
+        baseType <- QC.arbitrary
+        trace "test" $ return ()
+        numSubsts <- chooseLog (size baseType)
+        poss <- liftM (take numSubsts) $ nonOverlappingPos baseType
+        let subTerms = map (fromJust . subtermAt baseType) poss
+        let takenNames = S.fromList (getVarNames baseType)
+        let varPrefix = "mtyvar"
+        let freeNames = St.evalState (freeNamesM varPrefix) (takenNames, 1)
+        let names = St.evalState (mapM assignName subTerms) (M.empty, freeNames)
+        let vars = map VarT names
+        let substType = foldl (\term (subst, pos) -> substitute subst pos term) baseType (zip vars poss)
+        return $ MatchingTypes (baseType, substType)
+
+assignName :: (Ord t, Term t) => t -> St.State (M.Map t Name, [Name]) Name
+assignName term = do
+    (usedNames, nextName:freeNames) <- St.get
+    case M.lookup term usedNames of
+        Nothing   -> St.put (M.insert term nextName usedNames, freeNames) >> return nextName
+        Just name -> return name
+
+nextNameM :: String -> St.State (S.Set Name, Int) Name
+nextNameM prefix = do
+    takenNames <- St.gets fst
+    (name, idx) <- St.gets (uncurry $ nextNameIdx prefix)
+    St.put (name `S.insert` takenNames, idx+1)
+    return name
+
+freeNamesM :: String -> St.State (S.Set Name, Int) [Name]
+freeNamesM prefix = do
+    name <- nextNameM prefix
+    names <- freeNamesM prefix
+    return $ name : names
+
+nextNameIdx :: String -> S.Set Name -> Int -> (Name, Int)
+nextNameIdx prefix takenNames firstIdx =
+    let idxToName idx = mkName $ prefix ++ show idx
+        isTaken nm = nm `S.member` takenNames
+    in head $ filter (not . isTaken . fst) $ map (\idx -> (idxToName idx, idx)) [firstIdx..]
+
+chooseLog :: Integral a => a -> QC.Gen a
+chooseLog n = liftM (round . exp) $ QC.choose (0.0 :: Float, log (fromIntegral n))
+
+getAllPos :: Term t => t -> [Position]
+getAllPos t = (Root :) $ concat $ snd
+    $ mapAccumL (\i st -> (i+1, map (i°) (getAllPos st))) 0 (subterms t)
+
+nonOverlappingPos :: Term t => t -> QC.Gen [Position]
+nonOverlappingPos term = do
+    rposs <- shuffle $ getAllPos term
+    return $ nubBy overlap rposs
+
+overlap :: Position -> Position -> Bool
+overlap _ Root = True
+overlap Root _ = True
+overlap (Dot i p) (Dot i' p') | (i /= i') = False
+                              | otherwise = overlap p p'
+
+shuffle :: [a] -> QC.Gen [a]
+shuffle [] = return []
+shuffle xs = do
+  (y, ys) <- QC.elements (selectOne xs)
+  (y:) <$> shuffle ys
+  where
+    selectOne [] = []
+    selectOne (y:ys) = (y,ys) : map (second (y:)) (selectOne ys)
+
+second :: (b -> b') -> (a, b) -> (a, b')
+second f (x, y) = (x, f y)
+
hunk ./src/Tests.hs 202
-matchApply :: (Term t, Unify t) => t -> t -> t -> QC.Property
-matchApply _witness t1 t2 = runContext $ (do
+matchApplyC :: (Term t, Unify t) => t -> t -> t -> C (Either String) QCP.Property
+matchApplyC _witness t1 t2 = do
hunk ./src/Tests.hs 207
-    ) `safeCatchErrorC` const QC.discard
+
+matchApply :: (Term t, Unify t) => t -> t -> t -> QC.Property
+matchApply _witness t1 t2 = runContext $ matchApplyC _witness t1 t2
+    `safeCatchErrorC` const QC.discard
+
+matchApplyUnforgiving :: (Term t, Unify t) => t -> t -> t -> QC.Property
+matchApplyUnforgiving _witness t1 t2 = runContext $
+    either error return `mapReaderT` matchApplyC _witness t1 t2
hunk ./src/Tests.hs 220
-    testProperty "Exprs: apply (match a b) b == a" (matchApply texpWitness)
+    testProperty "Exprs: apply (match a b) b == a" (matchApply texpWitness),
+    testProperty "MatchingTypes: apply (match a b) b == a" (uncurry (matchApplyUnforgiving typeWitness) . getMatchingTypes)