From 67344007060f58263d1e9f837cd13985d9609359 Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Tue, 16 Feb 2021 15:42:33 -0800
Subject: [PATCH] More comments to illustrate how projections and type
 applications are supposed to interact.

---
 src/Cryptol/Parser/ParserUtils.hs | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs
index 3b770fb1..ff59dac4 100644
--- a/src/Cryptol/Parser/ParserUtils.hs
+++ b/src/Cryptol/Parser/ParserUtils.hs
@@ -299,6 +299,15 @@ mkEApp es@(eLast :| _) =
      [ f, x, `{ a = 2 }, y ]
      becomes
      [ f, x ` { a = 2 }, y ]
+
+     The parser associates field and tuple projectors that follow an
+     explicit type application onto the TTyApp term, so we also
+     have to unwind those projections and reapply them.  For example:
+
+     [ f, x, `{ a = 2 }.f.2, y ]
+     becomes
+     [ f, (x`{ a = 2 }).f.2, y ]
+
   -}
   cvtTypeParams e [] = pure (e :| [])
   cvtTypeParams e (p : ps) =