From 116cdfdda4cb1630a9694dd3bb9fe4e054d2186e Mon Sep 17 00:00:00 2001
From: simonpj <unknown>
Date: Fri, 16 Jul 1999 14:06:57 +0000
Subject: [PATCH] [project @ 1999-07-16 14:06:57 by simonpj] * Fix a bug in the
unifier that made the typechecker loop on a 5-line program from Sigbjorn.
The bug is documented near the fix, in
TcUnify.uUnboundVar
---
ghc/compiler/typecheck/TcUnify.lhs | 21 ++++++++++++++++++++-
1 file changed, 20 insertions(+), 1 deletion(-)
diff --git a/ghc/compiler/typecheck/TcUnify.lhs b/ghc/compiler/typecheck/TcUnify.lhs
index 0f037f6e5dde..09695e77fe2b 100644
--- a/ghc/compiler/typecheck/TcUnify.lhs
+++ b/ghc/compiler/typecheck/TcUnify.lhs
@@ -300,7 +300,26 @@ uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
ASSERT( isNotUsgTy ps_ty2 )
checkTcM (not (isSigTyVar tv1))
(failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
- tcPutTyVar tv1 ps_ty2 `thenNF_Tc_`
+
+ tcPutTyVar tv1 non_var_ty2 `thenNF_Tc_`
+ -- This used to say "ps_ty2" instead of "non_var_ty2"
+
+ -- But that led to an infinite loop in the type checker!
+ -- Consider
+ -- type A a = ()
+ --
+ -- f :: (A a -> a -> ()) -> ()
+ -- f = \ _ -> ()
+ --
+ -- x :: ()
+ -- x = f (\ x p -> p x)
+ --
+ -- Here, we try to match "t" with "A t", and succeed
+ -- because the unifier looks through synonyms. The occurs
+ -- check doesn't kick in because we are "really" binding "t" to "()",
+ -- but we *actually* bind "t" to "A t" if we store ps_ty2.
+ -- That leads the typechecker into an infinite loop later.
+
returnTc ()
where
occur_check ty = mapTc occur_check_tv (varSetElems (tyVarsOfType ty)) `thenTc_`
--
GitLab