- ; unless (equalLength tvs1 tvs2) (bale_out outer)
- ; traceTc (text "We're past the first length test")
- ; tvs <- tcInstSkolTyVars UnkSkol tvs1 -- Not a helpful SkolemInfo
- -- Get location from monad, not from tvs1
- ; let tys = mkTyVarTys tvs
- in_scope = mkInScopeSet (mkVarSet tvs)
- phi1 = substTy (mkTvSubst in_scope (zipTyEnv tvs1 tys)) body1
- phi2 = substTy (mkTvSubst in_scope (zipTyEnv tvs2 tys)) body2
- (theta1,tau1) = tcSplitPhiTy phi1
- (theta2,tau2) = tcSplitPhiTy phi2
-
- ; addErrCtxtM (unifyForAllCtxt tvs phi1 phi2) $ do
- { unless (equalLength theta1 theta2) (bale_out outer)
- ; cois <- uPreds outer nb1 theta1 nb2 theta2 -- TOMDO: do something with these pred_cois
- ; traceTc (text "TOMDO!")
- ; coi <- uTys nb1 tau1 nb2 tau2
-
- -- Check for escape; e.g. (forall a. a->b) ~ (forall a. a->a)
- ; free_tvs <- zonkTcTyVarsAndFV (varSetElems (tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2))
- ; when (any (`elemVarSet` free_tvs) tvs)
- (bleatEscapedTvs free_tvs tvs tvs)
-
- -- If both sides are inside a box, we are in a "box-meets-box"
- -- situation, and we should not have a polytype at all.
- -- If we get here we have two boxes, already filled with
- -- the same polytype... but it should be a monotype.
- -- This check comes last, because the error message is
- -- extremely unhelpful.
- ; when (nb1 && nb2) (notMonoType ty1)
- ; return coi
- }}
+ ; unless (equalLength tvs1 tvs2) (bale_out outer)
+ ; traceTc (text "We're past the first length test")
+ ; tvs <- tcInstSkolTyVars UnkSkol tvs1 -- Not a helpful SkolemInfo
+ -- Get location from monad, not from tvs1
+ ; let tys = mkTyVarTys tvs
+ in_scope = mkInScopeSet (mkVarSet tvs)
+ phi1 = substTy (mkTvSubst in_scope (zipTyEnv tvs1 tys)) body1
+ phi2 = substTy (mkTvSubst in_scope (zipTyEnv tvs2 tys)) body2
+ (theta1,tau1) = tcSplitPhiTy phi1
+ (theta2,tau2) = tcSplitPhiTy phi2
+
+ ; addErrCtxtM (unifyForAllCtxt tvs phi1 phi2) $ do
+ { unless (equalLength theta1 theta2) (bale_out outer)
+ ; _cois <- uPreds outer nb1 theta1 nb2 theta2 -- TOMDO: do something with these pred_cois
+ ; traceTc (text "TOMDO!")
+ ; coi <- uTys nb1 tau1 nb2 tau2
+
+ -- Check for escape; e.g. (forall a. a->b) ~ (forall a. a->a)
+ ; free_tvs <- zonkTcTyVarsAndFV (varSetElems (tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2))
+ ; when (any (`elemVarSet` free_tvs) tvs)
+ (bleatEscapedTvs free_tvs tvs tvs)
+
+ -- If both sides are inside a box, we are in a "box-meets-box"
+ -- situation, and we should not have a polytype at all.
+ -- If we get here we have two boxes, already filled with
+ -- the same polytype... but it should be a monotype.
+ -- This check comes last, because the error message is
+ -- extremely unhelpful.
+ ; when (nb1 && nb2) (notMonoType ty1)
+ ; return coi
+ }}