From: simonpj@microsoft.com <unknown>
Date: Mon, 11 Aug 2008 12:35:26 +0000 (+0000)
Subject: Fix Trac #2367: selectors for GADTs
X-Git-Url: http://git.megacz.com/?a=commitdiff_plain;h=77c6ba6f015933989594d167162265b5633f74e3;p=ghc-hetmet.git

Fix Trac #2367: selectors for GADTs

The generation of record selectors for GADTs and the like was
pretty screwed up.  This patch fixes it.

Note that Unify.refineType is now used only in the generation of
record seletctors -- but it really does seem to be needed there.

Thanks to Max for finding this bug.
---

diff --git a/compiler/basicTypes/MkId.lhs b/compiler/basicTypes/MkId.lhs
index 0e2d8b8..2262bbc 100644
--- a/compiler/basicTypes/MkId.lhs
+++ b/compiler/basicTypes/MkId.lhs
@@ -462,17 +462,29 @@ For GADTs, we require that all constructors with a common field 'f' have the sam
 result type (modulo alpha conversion).  [Checked in TcTyClsDecls.checkValidTyCon]
 E.g. 
         data T where
-          T1 { f :: a } :: T [a]
-          T2 { f :: a, y :: b  } :: T [a]
-and now the selector takes that type as its argument:
-        f :: forall a. T [a] -> a
-        f t = case t of
-                T1 { f = v } -> v
-                T2 { f = v } -> v
+          T1 { f :: Maybe a } :: T [a]
+          T2 { f :: Maybe a, y :: b  } :: T [a]
+
+and now the selector takes that result type as its argument:
+   f :: forall a. T [a] -> Maybe a
+
+Details: the "real" types of T1,T2 are:
+   T1 :: forall r a.   (r~[a]) => a -> T r
+   T2 :: forall r a b. (r~[a]) => a -> b -> T r
+
+So the selector loooks like this:
+   f :: forall a. T [a] -> Maybe a
+   f (a:*) (t:T [a])
+     = case t of
+	 T1 c   (g:[a]~[c]) (v:Maybe c)       -> v `cast` Maybe (right (sym g))
+         T2 c d (g:[a]~[c]) (v:Maybe c) (w:d) -> v `cast` Maybe (right (sym g))
+
 Note the forall'd tyvars of the selector are just the free tyvars
 of the result type; there may be other tyvars in the constructor's
 type (e.g. 'b' in T2).
 
+Note the need for casts in the result!
+
 Note [Selector running example]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 It's OK to combine GADTs and type families.  Here's a running example:
@@ -641,9 +653,7 @@ mkRecordSelId tycon field_label
         --      foo = /\a. \t:T. case t of { MkT f -> f a }
 
     mk_alt data_con
-      =   ASSERT2( data_ty `tcEqType` field_ty, 
-                   ppr data_con $$ ppr data_ty $$ ppr field_ty )
-          mkReboxingAlt rebox_uniqs data_con (ex_tvs ++ co_tvs ++ arg_vs) rhs
+      = mkReboxingAlt rebox_uniqs data_con (ex_tvs ++ co_tvs ++ arg_vs) rhs
       where
            -- get pattern binders with types appropriately instantiated
         arg_uniqs = map mkBuiltinUnique [arg_base..]
@@ -654,20 +664,21 @@ mkRecordSelId tycon field_label
         rebox_uniqs = map mkBuiltinUnique [rebox_base..]
 
         -- data T :: *->* where T1 { fld :: Maybe b } -> T [b]
-        --      Hence T1 :: forall a b. (a=[b]) => b -> T a
+        --      Hence T1 :: forall a b. (a~[b]) => b -> T a
         -- fld :: forall b. T [b] -> Maybe b
         -- fld = /\b.\(t:T[b]). case t of 
         --              T1 b' (c : [b]=[b']) (x:Maybe b') 
         --                      -> x `cast` Maybe (sym (right c))
 
-                -- Generate the refinement for b'=b, 
-                -- and apply to (Maybe b'), to get (Maybe b)
-        reft           = matchRefine co_tvs
-        the_arg_id_ty  = idType the_arg_id
-        (rhs, data_ty) = 
-          case refineType reft the_arg_id_ty of
-            Just (co, data_ty) -> (Cast (Var the_arg_id) co, data_ty)
-            Nothing            -> (Var the_arg_id, the_arg_id_ty)
+                -- Generate the cast for the result
+		-- See Note [GADT record selectors] for why a cast is needed
+	in_scope_tvs = ex_tvs ++ co_tvs ++ data_tvs
+        reft         = matchRefine in_scope_tvs (map (mkSymCoercion . mkTyVarTy) co_tvs)
+        rhs = case refineType reft (idType the_arg_id) of
+                Nothing            -> Var the_arg_id
+                Just (co, data_ty) -> ASSERT2( data_ty `tcEqType` field_ty, 
+	    	                        ppr data_con $$ ppr data_ty $$ ppr field_ty )
+          	       		      Cast (Var the_arg_id) co
 
         field_vs    = filter (not . isPredTy . idType) arg_vs 
         the_arg_id  = assoc "mkRecordSelId:mk_alt" 
diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs
index 7c8ad9d..c1ef798 100644
--- a/compiler/types/Unify.lhs
+++ b/compiler/types/Unify.lhs
@@ -442,7 +442,7 @@ refineResType reft ty
 %************************************************************************
 
 \begin{code}
-matchRefine :: [CoVar] -> Refinement
+matchRefine :: [TyVar] -> [Coercion] -> Refinement
 \end{code}
 
 Given a list of coercions, where for each coercion c::(ty1~ty2), the type ty2
@@ -462,19 +462,16 @@ Precondition: The rhs types must indeed be a specialisation of the lhs types;
 NB: matchRefine does *not* expand the type synonyms.
 
 \begin{code}
-matchRefine co_vars 
-  = Reft in_scope (foldr plusVarEnv emptyVarEnv (map refineOne co_vars))
+matchRefine in_scope_tvs cos 
+  = Reft in_scope (foldr plusVarEnv emptyVarEnv (map refineOne cos))
   where
-    in_scope = foldr extend emptyInScopeSet co_vars
+    in_scope = mkInScopeSet (mkVarSet in_scope_tvs)
+	-- NB: in_scope_tvs include both coercion variables
+	--     *and* the tyvars in their kinds
 
-	-- For each co_var, add it *and* the tyvars it mentions, to in_scope
-    extend co_var in_scope
-      = extendInScopeSetSet in_scope $
-	  extendVarSet (tyVarsOfType (tyVarKind co_var)) co_var
-
-    refineOne co_var = refine (TyVarTy co_var) ty1 ty2
+    refineOne co = refine co ty1 ty2
       where
-        (ty1, ty2) = splitCoercionKind (tyVarKind co_var)
+        (ty1, ty2) = coercionKind co
 
     refine co (TyVarTy tv) ty                     = unitVarEnv tv (co, ty)
     refine co (TyConApp _ tys) (TyConApp _ tys')  = refineArgs co tys tys'