Comments only
authorSimon Peyton Jones <simonpj@microsoft.com>
Thu, 10 May 2012 08:45:16 +0000 (09:45 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Thu, 10 May 2012 08:45:16 +0000 (09:45 +0100)
compiler/typecheck/TcEvidence.lhs

index 82298a4..83ecd8b 100644 (file)
@@ -455,10 +455,10 @@ evBindMapBinds bs
 data EvBind = EvBind EvVar EvTerm
 
 data EvTerm
-  = EvId EvId                    -- Term-level variable-to-variable bindings
-                                 -- (no coercion variables! they come via EvCoercion)
+  = EvId EvId                    -- Any sort of evidence Id, including coercions
 
-  | EvCoercion TcCoercion        -- (Boxed) coercion bindings
+  | EvCoercion TcCoercion        -- (Boxed) coercion bindings 
+                                 -- See Note [Coercion evidence terms]
 
   | EvCast EvTerm TcCoercion     -- d |> co
 
@@ -492,6 +492,29 @@ data EvLit
 
 \end{code}
 
+Note [Coecion evidence terms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Notice that a coercion variable (v :: t1 ~ t2) can be represented as an EvTerm
+in two different ways:
+   EvId v
+   EvCoercion (TcCoVarCo v)
+
+An alternative would be 
+
+* To establish the invariant that coercions are represented only 
+   by EvCoercion
+
+* To maintain the invariant by smart constructors.  Eg
+     mkEvCast (EvCoercion c1) c2 = EvCoercion (TcCastCo c1 c2)
+     mkEvCast t c = EvCast t c
+
+We do quite often need to get a TcCoercion from an EvTerm; see
+'evTermCoercion'.  Notice that as well as EvId and EvCoercion it may see
+an EvCast.
+
+I don't think it matters much... but maybe we'll find a good reason to
+do one or the other.
+
 Note [EvKindCast] 
 ~~~~~~~~~~~~~~~~~ 
 EvKindCast g kco is produced when we have a constraint (g : s1 ~ s2) 
@@ -581,6 +604,7 @@ isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"
 
 evTermCoercion :: EvTerm -> TcCoercion
 -- Applied only to EvTerms of type (s~t)
+-- See Note [Coercion evidence terms]
 evTermCoercion (EvId v)        = mkTcCoVarCo v
 evTermCoercion (EvCoercion co) = co
 evTermCoercion (EvCast tm co)  = TcCastCo (evTermCoercion tm) co