- | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
- | (_,_) ->
- raise
- (TypeCheckerFailure
- (NotWellTyped
- ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= "^ CicPp.ppterm t2')))
+ | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
+ (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
+ let t' = CicUniv.fresh() in
+ if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then
+ assert false ; (* not possible, error in CicUniv *)
+ C.Sort (C.Type t')
+ | (C.Sort _,C.Sort (C.Type t1)) ->
+ (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
+ C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *)
+ | (C.Meta _, C.Sort _) -> t2'
+ | (C.Meta _, (C.Meta (_,_) as t))
+ | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
+ t2'
+ | (_,_) -> raise (TypeCheckerFailure (sprintf
+ "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
+ (CicPp.ppterm t2')))