Refactor `DeclarationElaborator` and `FamilyCheck`

This issue is related to #11 (closed). As soon as we have a clear constraint-based unification and type checker, we can clean up the fixed-point computation for resolving modules (i.e., we can then first introduce the names with their respective check-constraints) and the elaboration of declarations overall.