← All traces

Refining a GADT match

get matches on a GADT, so each branch may assume a different equality. The typechecker chapter argues this one program shape is why constraint solving is deferred at all. Here is the solver actually doing it.

What you wrote.

{-# LANGUAGE GADTs #-}

-- The smallest program that forces an implication constraint: each branch of
-- `get` may assume a different equality, so each becomes its own implication
-- with its own Given.
module Refine where

data T a where
  TInt  :: T Int
  TBool :: T Bool

get :: T a -> a
get TInt  = 1
get TBool = True

What to look for

Typechecker trace → solveImplication
One implication per branch. Inside each: an Implic { ... } with its own TcLevel, its own skolems, and its own Given.
Typechecker trace → solveSimpleGivens
The branch assumption (the equality from the constructor) being installed as a fact before the branch body is checked against it.
Typechecker trace → the Inerts printouts
Innermost given equalities = 2 while a branch body is being solved, and = 0 outside it. Local assumptions are local, and the inert set says so in one line.