diff options
| author | Richard Eisenberg <eir@cis.upenn.edu> | 2015-06-05 09:50:00 -0400 |
|---|---|---|
| committer | Richard Eisenberg <eir@cis.upenn.edu> | 2015-06-05 11:09:24 -0400 |
| commit | 53c13744210402151e58baf0d703d23927f5188d (patch) | |
| tree | 3f8602750ceca3d2dc58119ff96740b55f20bf57 | |
| parent | 761fb7c4869a081da7320e4307dcb947b5ed95d1 (diff) | |
| download | haskell-53c13744210402151e58baf0d703d23927f5188d.tar.gz | |
Minor code cleanup
| -rw-r--r-- | compiler/typecheck/TcCanonical.hs | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index 122319420f..5bbab219a5 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -432,7 +432,7 @@ can_eq_nc' flat _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2 | Just ty2' <- tcView ty2 = can_eq_nc flat ev eq_rel ty1 ps_ty1 ty2' ps_ty2 -- need to check for reflexivity in the ReprEq case. --- See Note [AppTy reflexivity check] and Note [Eager reflexivity check] +-- See Note [Eager reflexivity check] can_eq_nc' _flat _rdr_env _envs ev ReprEq ty1 _ ty2 _ | ty1 `eqType` ty2 = canEqReflexive ev ReprEq ty1 @@ -509,11 +509,6 @@ can_eq_nc' True _rdr_env _envs ev NomEq ty1 _ (AppTy t2 s2) _ | Just (t1, s1) <- tcSplitAppTy_maybe ty1 = can_eq_app ev t1 s1 t2 s2 --- See Note [AppTy reflexivity check] -can_eq_nc' _flat _rdr_env _envs ev ReprEq ty1@(AppTy {}) _ ty2@(AppTy {}) _ - | ty1 `eqType` ty2 - = canEqReflexive ev ReprEq ty1 - -- No similarity in type structure detected. Flatten and try again! can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2 = do { (xi1, co1) <- flatten FM_FlattenAll ev ps_ty1 @@ -571,8 +566,7 @@ equality because the flattener technology deals with the similar case Note that this check does not catch all cases, but it will catch the cases we're most worried about, types like X above that are actually inhabited. -Note [AppTy reflexivity check] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Here's another place where this reflexivity check is key: Consider trying to prove (f a) ~R (f a). The AppTys in there can't be decomposed, because representational equality isn't congruent with respect to AppTy. So, when canonicalising the equality above, we get stuck and |