| What would be most flexible for the user is to return the best | information that is available. In the example: | | >NB This can apply to top-level decls too: | > f = 1+2 | > $( ... reify 'f... ) | > g = f + (4::Int) | > | >Because of the monomorphism restriction, the type of f is fixed by f's | >caller, which may be "after" the reification. | > | it might still be useful to find out that an approximation to the type | is f :: Num a => a, even though that isn't the final type. That would | suggest something like | | data TypeQuery a = ExactType a | ApproximationType a Actually, I was thinking of something more modest. The type of f will, at the stage of reification, be a -> a where a is an as-yet-refined internal type variable. If instead we had id x = x the type would be forall a. a->a So I'm thinking that if the Type returned to you by TH contains free type variables, that might simply signify types that might be later refined. Simple. But not very principled, because the type you see will depend on which order the type checker happens to do its work in. Simon