RAE's response to SPJ's question in flattening-notes
authorRichard Eisenberg <eir@cis.upenn.edu>
Mon, 8 Dec 2014 15:32:21 +0000 (10:32 -0500)
committerRichard Eisenberg <eir@cis.upenn.edu>
Mon, 8 Dec 2014 15:32:21 +0000 (10:32 -0500)
compiler/typecheck/Flattening-notes

index 35f2f2d..657e91e 100644 (file)
@@ -225,3 +225,8 @@ rewrite
 Well, it depends on the roles at which T uses its arguments :-(.
 So it may not be enough just to look at (flavour,role) pairs?
 
+RAE: This is true, but it is taken care of by being careful in the
+flattening algorithm. Flattening (T a) looks at the roles of
+T's parameters, and chooses the role for flattening `a` appropriately.
+This is why there must be the [Role] parameter to flattenMany.
+Of course, this non-uniform rewriting may gum up the proof works.