+badReftElts :: InternalReft -> [(Unique, (Coercion,Type))]
+-- Return the BAD elements of the refinement
+-- Should be empty; used in asserions only
+badReftElts env
+ = filter (not . ok) (ufmToList env)
+ where
+ ok :: (Unique, (Coercion, Type)) -> Bool
+ ok (u, (co, ty)) | Just tv <- tcGetTyVar_maybe ty1
+ = varUnique tv == u && ty `tcEqType` ty2
+ | otherwise = False
+ where
+ (ty1,ty2) = coercionKind co
+