Basic unification tests for type checkers

Basic type solver tests.hs

fineGrained :: Spec
fineGrained = do
  describe
    "Successful"
    (do it "a ~ a" (shouldReturn (unifyConstraints' [a .~ a]) (pure []))
        it
          "Integer ~ Integer"
          (shouldReturn (unifyConstraints' [_Integer .~ _Integer]) (pure []))
        it
          "a ~ b"
          (shouldReturn (unifyConstraints' [a .~ b]) (pure [a' .+-> b]))
        it
          "a ~ Integer"
          (shouldReturn
             (unifyConstraints' [a .~ _Integer])
             (pure [a' .+-> _Integer]))
        it
          "F a b ~ F Text a"
          (shouldReturn
             (unifyConstraints' [_F a b .~ _F _Text a])
             (pure [a' .+-> _Text, b' .+-> _Text]))
        it
          "F a Text ~ F Text a"
          (shouldReturn
             (unifyConstraints' [_F a _Text .~ _F _Text a])
             (pure [a' .+-> _Text]))
        it
          "F a Text ~ F Integer b"
          (shouldReturn
             (unifyConstraints' [_F a _Text .~ _F _Integer b])
             (pure [a' .+-> _Integer, b' .+-> _Text]))
        it
          "F a a ~ F (Option b) (Option Integer)"
          (shouldReturn
             (unifyConstraints' [_F a a .~ _F (_Option b) (_Option _Integer)])
             (pure [a' .+-> _Option _Integer, b' .+-> _Integer]))
        it
          "(t ~ F a a, F a a ~ F (Option b) (Option Integer)) => t"
          (shouldReturn
             (unifyAndSubstitute'
                [t .~ _F a a, _F a a .~ _F (_Option b) (_Option _Integer)]
                t)
             (pure (solveType mempty (_F (_Option _Integer) (_Option _Integer))))))
  describe
    "Failing"
    (do it
          "Occurs check: F a b ~ a"
          (shouldReturn
             (unifyConstraints' [_F a b .~ a])
             (Left (OccursCheckFail a' (_F a b))))
        it
          "Kind mismatch: F a ~ b"
          (shouldReturn
             (unifyConstraints' [_F_partial a .~ b])
             (Left (KindMismatch b' (_F_partial a))))
        it
          "Constant mismatch: Integer ~ Text"
          (shouldReturn
             (unifyConstraints' [_Integer .~ _Text])
             (Left (TypeMismatch (_Integer .~ _Text))))
        it
          "Type mismatch: F a a ~ F (Option Text) (Option Integer)"
          (shouldReturn
             (unifyConstraints'
                [_F a a .~ _F (_Option _Text) (_Option _Integer)])
             (Left (TypeMismatch (_Text .~ _Integer)))))