diff --git a/src/Tessera/Matrix.hs b/src/Tessera/Matrix.hs
new file mode 100644
index 0000000..dc508cf
--- /dev/null
+++ b/src/Tessera/Matrix.hs
@@ -0,0 +1,269 @@
+module Tessera.Matrix where
+
+import Data.List (foldl', sortBy)
+import Data.Maybe (mapMaybe)
+import Data.Ord (comparing)
+import qualified Data.Map.Strict as Map
+
+import Tessera.Env
+import Tessera.Syntax
+
+data Key
+  = KeyCon String
+  | KeyInt Integer
+  | KeyBool Bool
+  | KeyTuple Int
+  deriving (Eq, Show)
+
+data Signature
+  = FiniteSignature [(Key, [Type])]
+  | IntegerSignature
+  deriving (Eq, Show)
+
+data Outcome
+  = NotCovered [Pattern]
+  | Covered
+  | SearchExhausted
+  deriving (Eq, Show)
+
+signature :: Env -> Type -> Signature
+signature env ty = case ty of
+  TName "Int" [] -> IntegerSignature
+  TName "Bool" [] -> FiniteSignature [(KeyBool True, []), (KeyBool False, [])]
+  TName name arguments -> case lookupType env name of
+    Just definition
+      | not (Map.findWithDefault True name (finiteInhabitants env)) -> FiniteSignature []
+      | otherwise ->
+          FiniteSignature
+            [ (KeyCon (constructorName c), instantiate (typeDefinitionParams definition) arguments (constructorArgs c))
+            | c <- typeDefinitionConstructors definition
+            ]
+    Nothing -> FiniteSignature []
+  TTuple elements -> FiniteSignature [(KeyTuple (length elements), elements)]
+  TVar _ -> FiniteSignature []
+
+headKey :: Pattern -> Maybe Key
+headKey pattern' = case pattern' of
+  PCon name _ -> Just (KeyCon name)
+  PInt n -> Just (KeyInt n)
+  PBool b -> Just (KeyBool b)
+  PTuple elements -> Just (KeyTuple (length elements))
+  PVar _ -> Nothing
+  PWild -> Nothing
+
+isVariable :: Pattern -> Bool
+isVariable pattern' = case pattern' of
+  PVar _ -> True
+  PWild -> True
+  _ -> False
+
+patternArguments :: Pattern -> [Pattern]
+patternArguments pattern' = case pattern' of
+  PCon _ arguments -> arguments
+  PTuple elements -> elements
+  _ -> []
+
+keyArity :: Env -> Key -> Int
+keyArity env key = case key of
+  KeyCon name -> maybe 0 id (constructorArity env name)
+  KeyBool _ -> 0
+  KeyInt _ -> 0
+  KeyTuple n -> n
+
+buildKey :: Key -> [Pattern] -> Pattern
+buildKey key arguments = case key of
+  KeyCon name -> PCon name arguments
+  KeyBool b -> PBool b
+  KeyInt n -> PInt n
+  KeyTuple n -> PTuple (take n arguments)
+
+specialize :: Env -> Key -> [[Pattern]] -> [[Pattern]]
+specialize env key = concatMap step
+  where
+    arity = keyArity env key
+    step row = case row of
+      [] -> []
+      (p : rest)
+        | isVariable p -> [replicate arity PWild ++ rest]
+        | headKey p == Just key -> [patternArguments p ++ rest]
+        | otherwise -> []
+
+defaultMatrix :: [[Pattern]] -> [[Pattern]]
+defaultMatrix = mapMaybe step
+  where
+    step row = case row of
+      (p : rest) | isVariable p -> Just rest
+      _ -> Nothing
+
+allConstructorsPresent :: [(Key, [Type])] -> [Pattern] -> Bool
+allConstructorsPresent constructors column =
+  all (\(key, _) -> key `elem` mapMaybe headKey column) constructors
+
+inhabitedType :: Env -> [String] -> Type -> Bool
+inhabitedType env visited ty = case ty of
+  TVar _ -> True
+  TTuple elements -> all (inhabitedType env visited) elements
+  TName "Int" _ -> True
+  TName "Bool" _ -> True
+  TName name arguments
+    | name `elem` visited -> False
+    | otherwise -> case lookupType env name of
+        Just definition ->
+          any (constructorInhabited (name : visited)) (typeDefinitionConstructors definition)
+          where
+            constructorInhabited seen c =
+              all (inhabitedType env seen) (instantiate (typeDefinitionParams definition) arguments (constructorArgs c))
+        Nothing -> False
+
+sample :: Env -> Int -> Type -> Pattern
+sample env limit ty
+  | limit <= 0 = PWild
+  | otherwise = case ty of
+      TVar _ -> PWild
+      TName "Int" _ -> PInt 0
+      TName "Bool" _ -> PBool False
+      TTuple elements -> PTuple (map (sample env (limit - 1)) elements)
+      TName name arguments -> case lookupType env name of
+        Just definition ->
+          let candidates =
+                [ (c, instantiate (typeDefinitionParams definition) arguments (constructorArgs c))
+                | c <- typeDefinitionConstructors definition
+                ]
+              usable =
+                [ (c, argumentTypes)
+                | (c, argumentTypes) <- candidates
+                , all (inhabitedType env []) argumentTypes
+                ]
+              ordered = sortBy (comparing (length . snd)) usable
+          in case ordered of
+              ((c, argumentTypes) : _) ->
+                PCon (constructorName c) (map (sample env (limit - 1)) argumentTypes)
+              [] -> PWild
+        Nothing -> PWild
+
+sampleRow :: Env -> Int -> [Type] -> [Pattern]
+sampleRow env limit = map (sample env limit)
+
+finiteInhabitants :: Env -> Map.Map String Bool
+finiteInhabitants env = iterateUntilEqual Map.empty
+  where
+    names = Map.keys (envTypes env)
+    iterateUntilEqual known =
+      let next = Map.fromList [(name, hasInhabitant known name) | name <- names]
+      in if next == known then known else iterateUntilEqual next
+    hasInhabitant known name
+      | name `elem` ["Int", "Bool"] = True
+      | otherwise = case lookupType env name of
+          Just definition -> any (all (argumentInhabited known) . constructorArgs) (typeDefinitionConstructors definition)
+          Nothing -> False
+    argumentInhabited known ty = case ty of
+      TVar _ -> True
+      TName name _ -> Map.findWithDefault False name known
+      TTuple elements -> all (argumentInhabited known) elements
+
+freshInteger :: [Integer] -> Integer
+freshInteger used = head [n | n <- [0 ..], n `notElem` used]
+
+firstJust :: [Maybe a] -> Maybe a
+firstJust [] = Nothing
+firstJust (Just x : _) = Just x
+firstJust (Nothing : rest) = firstJust rest
+
+witness :: Env -> Int -> [Type] -> [[Pattern]] -> Outcome
+witness env limit types matrix
+  | limit <= 0 = SearchExhausted
+  | null types = if null matrix then NotCovered [] else Covered
+  | otherwise = case signature env (head types) of
+      IntegerSignature -> integerWitness env (limit - 1) types matrix
+      FiniteSignature constructors ->
+        let column = map head matrix
+            complete = allConstructorsPresent constructors column
+        in if complete
+            then combine (map (branch constructors matrix types) constructors)
+            else case witness env (limit - 1) (tail types) (defaultMatrix matrix) of
+              NotCovered rest ->
+                case [ (key, argumentTypes) | (key, argumentTypes) <- constructors, key `notElem` mapMaybe headKey column ] of
+                  ((key, argumentTypes) : _) ->
+                    NotCovered (buildKey key (sampleRow env (limit - 1) argumentTypes) : rest)
+                  [] -> Covered
+              Covered -> Covered
+              SearchExhausted -> SearchExhausted
+  where
+    branch constructors' matrix' types' (key, argumentTypes) =
+      case witness env (limit - 1) (argumentTypes ++ tail types') (specialize env key matrix') of
+        NotCovered result ->
+          let arity = length argumentTypes
+          in NotCovered (buildKey key (take arity result) : drop arity result)
+        Covered -> Covered
+        SearchExhausted -> SearchExhausted
+
+    combine outcomes = case [rest | NotCovered rest <- outcomes] of
+      (rest : _) -> NotCovered rest
+      [] -> if SearchExhausted `elem` outcomes then SearchExhausted else Covered
+
+integerWitness :: Env -> Int -> [Type] -> [[Pattern]] -> Outcome
+integerWitness env limit types matrix =
+  let column = map head matrix
+      hasVariable = any isVariable column
+      literals = [n | PInt n <- column]
+  in if hasVariable
+      then case witness env limit (tail types) (defaultMatrix matrix) of
+        NotCovered rest -> NotCovered (PInt (freshInteger literals) : rest)
+        Covered -> Covered
+        SearchExhausted -> SearchExhausted
+      else NotCovered (PInt (freshInteger literals) : sampleRow env limit (tail types))
+
+useful :: Env -> [Type] -> [[Pattern]] -> [Pattern] -> Bool
+useful env types matrix query
+  | null query = null matrix
+  | otherwise = case query of
+      (p : rest) -> case headKey p of
+        Just key ->
+          useful env (keyArgumentTypes env (head types) key ++ tail types) (specialize env key matrix) (patternArguments p ++ rest)
+        Nothing -> case signature env (head types) of
+          IntegerSignature -> useful env (tail types) (defaultMatrix matrix) rest
+          FiniteSignature constructors ->
+            if allConstructorsPresent constructors (map head matrix)
+              then any (branch constructors matrix types rest) constructors
+              else useful env (tail types) (defaultMatrix matrix) rest
+  where
+    branch constructors' matrix' types' rest (key, argumentTypes) =
+      useful env (argumentTypes ++ tail types') (specialize env key matrix') (replicate (length argumentTypes) PWild ++ rest)
+
+keyArgumentTypes :: Env -> Type -> Key -> [Type]
+keyArgumentTypes env ty key = case signature env ty of
+  FiniteSignature constructors -> maybe [] id (lookup key constructors)
+  IntegerSignature -> []
+
+usefulWith :: Env -> [Type] -> [[Pattern]] -> [Pattern] -> Outcome
+usefulWith env types matrix query
+  | null query = if null matrix then NotCovered [] else Covered
+  | otherwise = case query of
+      (p : rest) -> case headKey p of
+        Just key -> case witness env 200 (keyArgumentTypes env (head types) key ++ tail types) (specialize env key matrix) of
+          NotCovered result ->
+            let arity = length (patternArguments p)
+            in NotCovered (buildKey key (take arity result) : drop arity result)
+          Covered -> Covered
+          SearchExhausted -> SearchExhausted
+        Nothing -> case signature env (head types) of
+          IntegerSignature -> usefulWith env (tail types) (defaultMatrix matrix) rest
+          FiniteSignature constructors ->
+            if allConstructorsPresent constructors (map head matrix)
+              then combine [ branch constructors matrix types rest c | c <- constructors ]
+              else usefulWith env (tail types) (defaultMatrix matrix) rest
+  where
+    branch constructors' matrix' types' rest (key, argumentTypes) =
+      usefulWith env (argumentTypes ++ tail types') (specialize env key matrix') (replicate (length argumentTypes) PWild ++ rest)
+
+    combine outcomes = case [result | NotCovered result <- outcomes] of
+      (result : _) -> NotCovered result
+      [] -> if SearchExhausted `elem` outcomes then SearchExhausted else Covered
+
+matrixRows :: [[Pattern]] -> Int
+matrixRows = length
+
+coverCheck :: Env -> [Type] -> [[Pattern]] -> Pattern -> Bool
+coverCheck env types matrix value =
+  let row = [value]
+  in useful env types matrix row
diff --git a/src/Tessera/Tree.hs b/src/Tessera/Tree.hs
new file mode 100644
index 0000000..7779fe5
--- /dev/null
+++ b/src/Tessera/Tree.hs
@@ -0,0 +1,134 @@
+module Tessera.Tree where
+
+import Data.List (foldl')
+import Data.Maybe (mapMaybe)
+
+import Tessera.Env
+import Tessera.Matrix
+import Tessera.Syntax
+
+data Occurrence = Occurrence [Int] deriving (Eq, Show)
+
+data Tree
+  = Success Int
+  | Failure
+  | Switch Occurrence [(Key, Tree)] (Maybe Tree)
+  | Bind Occurrence String Tree
+  deriving (Eq, Show)
+
+data Strategy = Leftmost | Heuristic deriving (Eq, Show)
+
+strategyName :: Strategy -> String
+strategyName Leftmost = "leftmost"
+strategyName Heuristic = "heuristic"
+
+removeAt :: Int -> [a] -> [a]
+removeAt index items = take index items ++ drop (index + 1) items
+
+type Row = ([Pattern], Int)
+
+specializeRows :: Env -> Key -> [Row] -> [Row]
+specializeRows env key = concatMap step
+  where
+    arity = keyArity env key
+    step (row, index) = case row of
+      [] -> []
+      (p : rest)
+        | isVariable p -> [(replicate arity PWild ++ rest, index)]
+        | headKey p == Just key -> [(patternArguments p ++ rest, index)]
+        | otherwise -> []
+
+defaultRows :: [Row] -> [Row]
+defaultRows = mapMaybe step
+  where
+    step (row, index) = case row of
+      (p : rest) | isVariable p -> Just (rest, index)
+      _ -> Nothing
+
+compileMatch :: Env -> Strategy -> [Type] -> [Row] -> [Occurrence] -> Tree
+compileMatch env strategy types rows occurrences
+  | null rows = Failure
+  | all isVariable (fst (head rows)) =
+      let (row, index) = head rows
+      in foldr bindVariable (Success index) (zip row occurrences)
+  | otherwise =
+      let patterns = map fst rows
+          column = chooseColumn strategy patterns
+          columnType = types !! column
+          occurrence = occurrences !! column
+          restTypes = removeAt column types
+          restOccurrences = removeAt column occurrences
+          columnPatterns = map (!! column) patterns
+          appearing = mapMaybe headKey columnPatterns
+          path = occurrencePath occurrence
+      in case signature env columnType of
+          IntegerSignature ->
+            let literals = [n | KeyInt n <- appearing]
+                branches =
+                  [ (KeyInt n, compileMatch env strategy restTypes (specializeRows env (KeyInt n) rows) restOccurrences)
+                  | n <- literals
+                  ]
+                defaultBranch =
+                  if any isVariable columnPatterns
+                    then Just (compileMatch env strategy restTypes (defaultRows rows) restOccurrences)
+                    else Nothing
+            in Switch occurrence branches defaultBranch
+          FiniteSignature constructors ->
+            let keys = map fst constructors
+                complete = allConstructorsPresent constructors columnPatterns
+                branchKeys = if complete then keys else [k | k <- keys, k `elem` appearing]
+                branches =
+                  [ ( key
+                    , compileMatch env strategy (argumentTypes ++ restTypes) (specializeRows env key rows) (argumentOccurrences ++ restOccurrences)
+                    )
+                  | key <- branchKeys
+                  , let argumentTypes = maybe [] id (lookup key constructors)
+                  , let argumentOccurrences = [Occurrence (path ++ [j]) | j <- [0 .. length argumentTypes - 1]]
+                  ]
+                defaultBranch =
+                  if not complete && not (null (defaultRows rows))
+                    then Just (compileMatch env strategy restTypes (defaultRows rows) restOccurrences)
+                    else Nothing
+            in Switch occurrence branches defaultBranch
+  where
+    bindVariable (pattern', occurrence) inner = case pattern' of
+      PVar name -> Bind occurrence name inner
+      _ -> inner
+
+occurrencePath :: Occurrence -> [Int]
+occurrencePath (Occurrence path) = path
+
+chooseColumn :: Strategy -> [[Pattern]] -> Int
+chooseColumn Leftmost matrix = head candidates
+  where candidates = [i | i <- [0 .. width - 1], not (isVariable (head matrix !! i))]
+        width = length (head matrix)
+chooseColumn Heuristic matrix = foldl' better (head candidates) (tail candidates)
+  where
+    width = length (head matrix)
+    candidates = [i | i <- [0 .. width - 1], not (isVariable (head matrix !! i))]
+    better best candidate =
+      let score i = (distinctKeys i, negate (constructorCount i), i)
+      in if score candidate < score best then candidate else best
+    distinctKeys i = length (unique [k | Just k <- map (headKey . (!! i)) matrix])
+    constructorCount i = length [() | row <- matrix, not (isVariable (row !! i))]
+    unique = foldl' (\acc x -> if x `elem` acc then acc else acc ++ [x]) []
+
+initialOccurrences :: Int -> [Occurrence]
+initialOccurrences n = [Occurrence [i] | i <- [0 .. n - 1]]
+
+treeSize :: Tree -> Int
+treeSize tree = case tree of
+  Success _ -> 1
+  Failure -> 1
+  Bind _ _ inner -> 1 + treeSize inner
+  Switch _ branches fallback -> 1 + sum (map (treeSize . snd) branches) + maybe 0 treeSize fallback
+
+treeDepth :: Tree -> Int
+treeDepth tree = case tree of
+  Success _ -> 1
+  Failure -> 1
+  Bind _ _ inner -> 1 + treeDepth inner
+  Switch _ branches fallback ->
+    let branchDepth = maximum (0 : map (treeDepth . snd) branches)
+        fallbackDepth = maybe 0 treeDepth fallback
+    in 1 + max branchDepth fallbackDepth