Add UnsolvedConstr type.
Use one variable.
Make codes more abstract
Support the forall type on type context.