Redo type checker using "propagate types inward" trick

[byorgey]

Peyton Jones et al, in section 5.4 of Practical type inference for arbitrary-rank types, describe an apparently well-known trick for improving type error messages: instead of an infer function, write a check function which takes an expected type; we can then recover infer by simply generating a fresh unification variable and passing that along as the "expected type".

I hope this may lay the groundwork for better error messages when type inference fails.

[TristanCacqueray]

To add source location to the TypeErr message, I tried to thread a TermLoc data into the TypeF and ideed that seems rather tricky =)

My first attempt looks like this:

data TermLoc = TermLoc {start :: Int, end :: Int}
  deriving (Eq, Show, Data)

-- Add TermLoc to the relevant terms
data Term
  = TVar TermLoc Var
  | TDef TermLoc Var (Maybe Polytype) Term
  | ...

which could be parsed like so:

locatedTerm :: (TermLoc -> a -> Term) -> Parser a -> Parser Term
locatedTerm mkTerm parser = do
  start <- getOffset
  a <- parser
  end <- getOffset
  pure $ mkTerm (TermLoc start' end') a

so that we could add the location of UnboundVar and DefNotTopLevel type errors. This is a rather simple solution, could it also work for the "propagate types inward" trick?

[byorgey]

To add source location to the TypeErr message, I tried to thread a TermLoc data into the TypeF and ideed that seems rather tricky =)

Note that to add a TermLoc to types, instead of adding it to TypeF directly, it could probably be done something like so:

type Type = Fix (Compose ((,) TermLoc) TypeF)

with lots of utility functions and pattern synonyms to make it not painful to use. Being able to easily decorate every node like this is one of the benefits of using a two-level type. Off the top of my head though I'm not sure how this would interact with unification; we would need to tell the library to not worry about TermLocs that don't match.

However, in any case I'm not sure adding TermLocs to types like this makes sense. Lots of Type values arise in ways that don't correspond to a particular place in the code.

Yes, if we do the "propagate types inward" trick, we could probably pick up a TermLoc from the term we are processing at the point where we get a unification failure. Pointing to the term where unification happened to fail is a notoriously bad way to identify the real location of the error, but it would be way better than nothing.

[TristanCacqueray]

Thank you for all the details. I'd rather wait for a new type checker implementation that could use the failing term loc when throwing the error, than fiddling with the current library.

You also mention another solution you'd like to try in #100 , and perhaps there is another technique we can use to manage the loc. For example, the Dhall.Core.Expr data type is using a Note Src Expr constructor to wrap terms when needed.

[TristanCacqueray]

As another example, the Grace.Syntax is using something like data Syntax = Syntax { loc : TermLoc, term : Term } where the recursive Term use that Syntax type to keep track of nested loc. Similarly the Grace.Type uses a similar technique.

[byorgey]

As another example, the Grace.Syntax is using something like data Syntax = Syntax { loc : TermLoc, term : Term } where the recursive Term use that Syntax type to keep track of nested loc.

Yes, that's a nicer approach than manually adding a TermLoc to every constructor of Term. It's isomorphic to the Fix (Compose ((,) TermLoc) thing.

[byorgey]

I spent a little more time thinking about this and think I understand why it would be an improvement. Suppose we have a definition like this:

def p : int * int = (3, true)

We call check on the body of the definition with the given type signature. But what happens now is that we then immediately switch to calling infer, which tries to infer some type for the body (in this case int * bool), and then generates a constraint that the given type int * int must be equal to the inferred type int * bool. This constraint is then given to the constraint solver, which eventually complains that it can't unify int and bool. But at that point we don't really know where the constraint came from.

But what if instead of having infer do most of the work, we have check do most of the work. Checking that a pair has a product type would turn into recursive checks that the left and right sides have the specified types. In this example we would reach a point where we are checking that true has type int, which would raise an error---but at this point we know exactly which part of the term we are checking, and we can indicate that in the error message.

This doesn't always work, and there are still other problems (such as the fact that the place where it actually fails might not be the real error at all), but it's still better than what we have now.

[byorgey]

As a proof of concept, I started by modifying the check function to look like this:

-- | @check t ty@ checks that @t@ has type @ty@.
check :: Syntax -> UType -> Infer ()
check s@(Syntax _ t) ty = case t of
  SPair s1 s2 -> do
    (ty1, ty2) <- decomposeProdTy ty
    check s1 ty1
    check s2 ty2
  _ -> do
    ty' <- infer s
    _ <- ty =:= ty'
    return ()

decomposeProdTy :: UType -> Infer (UType, UType)
decomposeProdTy (UTyProd ty1 ty2) = return (ty1, ty2)
decomposeProdTy ty = do
  ty1 <- fresh
  ty2 <- fresh
  ty =:= UTyProd ty1 ty2
  return (ty1, ty2)

I put this on the feature/propagate-types branch.

It doesn't yet produce any better error messages, but I think this proves that we can improve things incrementally, without having to do an entire rewrite of the typechecker. To actually get better error messages, we have to try as hard as possible to catch errors that we can flag right at checking time, instead of putting them all off to the unifier. For example, in this case once we recursively check that 3 and true both have type int, when we get to the call to check true int, we need to notice that true must have type bool, and that we can immediately throw an error using the specific SrcLoc info we have, since we have a concrete type int that we can see is not equal to bool without having to call the unifier (as opposed to something like a unification variable). We'll probably want to make a variant of =:= which does some concrete checking first before generating a unification constraint only as a last resort.