Type inference weirdness in the presence of type synonyms with unused arguments

[brianhuffman]

Fun fact: You can get the cryptol type checker to infer, for a closed expression, a type that contains an unresolved unification variable. Here's the source file:

type Int n = Integer

foo : {n} (fin n) => [n] -> Int n
foo x = `n

Loading module Cryptol
Loading module Main
[warning] at foo.cry:6:10--6:11 Unused name: n
[warning] at foo.cry:6:6--6:9:
  Assuming  n to have a numeric type
Main> :t foo 0x0
foo 0x0 : Int n`941

This is caused by an apparent bug in the definition of type variable substitution for cryptol types. When I saw the following case in the definition of apSubstMaybe (which is supposed to return Just t' to indicate that the substitution did something, and Nothing to indicate that the substitution left the value unchanged) I thought it was probably wrong and so I constructed this example to check.

cryptol/src/Cryptol/TypeCheck/Subst.hs

Lines 212 to 213 in ac0aca1

	TUser f ts t -> do t1 <- apSubstMaybe su t
	return (TUser f (map (apSubst su) ts) t1)

The constructor TUser contains both a list of the type synonym arguments, and also the body of the type synonym's definition. It's possible to define a type synonym in Cryptol whose body doesn't use all the arguments. But this code assumes that if the body is unchanged by the substitution, then the arguments will also be unchanged. The above example violates this assumption.