Improve core linter so it catches unsafeCoerce problems (T9122)

Summary:
This is a draft of the patch that is sent for review.

In this patch required changes in linter were introduced
and actual check:

 - new helper function: primRepSizeB
 - primRep check for floating
 - Add access to dynamic flags in linter.
 - Implement additional lint rules.

Reviewers: austin, goldfire, simonpj

Reviewed By: simonpj

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D637

GHC Trac Issues: #9122

4 files changed, 19 insertions, 3 deletions

diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott
index 56b4b99151..6015731257 100644
--- a/docs/core-spec/CoreLint.ott
+++ b/docs/core-spec/CoreLint.ott
@@ -207,9 +207,11 @@ k /= BOX
 ----------------------- :: CoVarCoRepr
 G |-co z_(s ~R#k t) : s ~Rep k t
 
-G |-ty t1 : k
------------------------------ :: UnivCo
-G |-co t1 ==>!_R t2 : t1 ~R k t2
+G |-ty t1 : k1
+G |-ty t2 : k2
+R <= Phant \/ not (k1 <: OpenKind) \/ not (k2 <: OpenKind) \/ compatibleUnBoxedTys t1 t2
+------------------------------------------------------------------------ :: UnivCo
+G |-co t1 ==>!_R t2 : t1 ~R k2 t2
 
 G |-co g : t1 ~R k t2
 ------------------------- :: SymCo
diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott
index 0c5b30483e..d64667af18 100644
--- a/docs/core-spec/CoreSyn.ott
+++ b/docs/core-spec/CoreSyn.ott
@@ -278,6 +278,7 @@ terminals :: 'terminals_' ::=
   | vars_of      ::   :: vars_of          {{ tex \textsf{vars\_of } }}
   | not          ::   :: not              {{ tex \neg }}
   | isUnLiftedTyCon :: :: isUnLiftenTyCon {{ tex \textsf{isUnLiftedTyCon} }}
+  | compatibleUnBoxedTys :: :: compatibleUnBoxedTys {{ tex \textsf{compatibleUnBoxedTys} }}
   | false        ::   :: false            {{ tex \textsf{false} }}
   | true         ::   :: true             {{ tex \textsf{true} }}
   | \/           ::   :: or               {{ tex \vee }}
@@ -333,6 +334,7 @@ formula :: 'formula_' ::=
   | no_duplicates </ bindingi // i />  ::   :: no_duplicates_binding
   | not formula                        ::   :: not
   | isUnLiftedTyCon T                  ::   :: isUnLiftedTyCon
+  | compatibleUnBoxedTys t1 t2         ::   :: compatibleUnBoxedTys
   | formula1 /\ formula2               ::   :: and
   | formula1 \/ formula2               ::   :: or
   | ( formula )                        ::   :: parens
diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng
index 28540ac8e9..ddbc6147d4 100644
--- a/docs/core-spec/core-spec.mng
+++ b/docs/core-spec/core-spec.mng
@@ -196,6 +196,18 @@ a list of coercions. This is elided in this presentation, as we simply identify
 axiom rules by their names $[[M]]$. See also \coderef{typecheck/TcTypeNats.lhs}{mkBinAxiom}
 and \coderef{typecheck/TcTypeNats.lhs}{mkAxiom1}.
 
+In \ottdrulename{Co\_UnivCo}, function $ \textsf{compatibleUnBoxedTys} $ stands for following checks:
+\begin{itemize}
+    \item both types are unboxed;
+    \item types should have same size;
+    \item both types should be either integral or floating;
+    \item coercion between vector types are not allowed;
+    \item unboxed tuples should have same length and each element should be coercible to
+    appropriate element of the target tuple;
+\end{itemize}
+For function implementation see \coderef{coreSyn/CoreLint.lhs}{checkTypes}.
+For futher discussion see \url{https://ghc.haskell.org/trac/ghc/wiki/BadUnsafeCoercions}.
+
 \subsection{Type constructors}
 
 Type constructors in GHC contain \emph{lots} of information. We leave most of it out
diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf
index 52f2e39f83..8d2e5cbb13 100644
--- a/docs/core-spec/core-spec.pdf
+++ b/docs/core-spec/core-spec.pdf