Fix Trac #8138.

The code in CoreLint did not take into account the possibility of
~R# arguments to functions. These can arise in argToPat in SpecConstr.
Now, CoreLint does not fail when it sees a ~R# parameter.

This commit also updates the core-spec document accordingly.

3 files changed, 5 insertions, 2 deletions

diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs
index 5befacdd45..68aaea5b5c 100644
--- a/compiler/coreSyn/CoreLint.lhs
+++ b/compiler/coreSyn/CoreLint.lhs
@@ -401,7 +401,6 @@ lintCoreExpr (Type ty)
 
 lintCoreExpr (Coercion co)
   = do { (_kind, ty1, ty2, role) <- lintInCo co
-       ; checkRole co Nominal role
        ; return (mkCoercionType role ty1 ty2) }
 
 \end{code}
diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott
index c2dba49612..f2799841dc 100644
--- a/docs/core-spec/CoreLint.ott
+++ b/docs/core-spec/CoreLint.ott
@@ -122,9 +122,13 @@ G |-ty t : k2
 G |-tm case e as z_s return t of </ alti // i /> : t
 
 G |-co g : t1 ~Nom k t2
--------------------- :: Coercion
+-------------------- :: CoercionNom
 G |-tm g : t1 ~#k t2
 
+G |-co g : t1 ~Rep k t2
+----------------------- :: CoercionRep
+G |-tm g : (~R#) k t1 t2
+
 defn G  |- name n ok ::  :: lintSingleBinding_lintBinder :: 'Name_'
   {{ com Name consistency check, \coderef{coreSyn/CoreLint.lhs}{lintSingleBinding\#lintBinder} }}
   {{ tex [[G]] \labeledjudge{n} [[n]] [[ok]] }}
diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf
index cb21286abb..4e4ca924fb 100644
--- a/docs/core-spec/core-spec.pdf
+++ b/docs/core-spec/core-spec.pdf