Add AnonArgFlag to FunTy

The big payload of this patch is:

  Add an AnonArgFlag to the FunTy constructor
  of Type, so that
    (FunTy VisArg   t1 t2) means (t1 -> t2)
    (FunTy InvisArg t1 t2) means (t1 => t2)

The big payoff is that we have a simple, local test to make
when decomposing a type, leading to many fewer calls to
isPredTy. To me the code seems a lot tidier, and probably
more efficient (isPredTy has to take the kind of the type).

See Note [Function types] in TyCoRep.

There are lots of consequences

* I made FunTy into a record, so that it'll be easier
  when we add a linearity field, something that is coming
  down the road.

* Lots of code gets touched in a routine way, simply because it
  pattern matches on FunTy.

* I wanted to make a pattern synonym for (FunTy2 arg res), which
  picks out just the argument and result type from the record. But
  alas the pattern-match overlap checker has a heart attack, and
  either reports false positives, or takes too long.  In the end
  I gave up on pattern synonyms.

  There's some commented-out code in TyCoRep that shows what I
  wanted to do.

* Much more clarity about predicate types, constraint types
  and (in particular) equality constraints in kinds.  See TyCoRep
  Note [Types for coercions, predicates, and evidence]
  and Note [Constraints in kinds].

  This made me realise that we need an AnonArgFlag on
  AnonTCB in a TyConBinder, something that was really plain
  wrong before. See TyCon Note [AnonTCB InivsArg]

* When building function types we must know whether we
  need VisArg (mkVisFunTy) or InvisArg (mkInvisFunTy).
  This turned out to be pretty easy in practice.

* Pretty-printing of types, esp in IfaceType, gets
  tidier, because we were already recording the (->)
  vs (=>) distinction in an ad-hoc way.  Death to
  IfaceFunTy.

* mkLamType needs to keep track of whether it is building
  (t1 -> t2) or (t1 => t2).  See Type
  Note [mkLamType: dictionary arguments]

Other minor stuff

* Some tidy-up in validity checking involving constraints;
  Trac #16263

7 files changed, 20 insertions, 21 deletions

diff --git a/testsuite/tests/callarity/unittest/CallArity1.hs b/testsuite/tests/callarity/unittest/CallArity1.hs
index 1100ff6a8f..00583d0209 100644
--- a/testsuite/tests/callarity/unittest/CallArity1.hs
+++ b/testsuite/tests/callarity/unittest/CallArity1.hs
@@ -27,16 +27,16 @@ import FastString
 go, go2, x, d, n, y, z, scrutf, scruta :: Id
 [go, go2, x,d, n, y, z, scrutf, scruta, f] = mkTestIds
     (words "go go2 x d n y z scrutf scruta f")
-    [ mkFunTys [intTy, intTy] intTy
-    , mkFunTys [intTy, intTy] intTy
+    [ mkVisFunTys [intTy, intTy] intTy
+    , mkVisFunTys [intTy, intTy] intTy
     , intTy
-    , mkFunTys [intTy] intTy
-    , mkFunTys [intTy] intTy
+    , mkVisFunTys [intTy] intTy
+    , mkVisFunTys [intTy] intTy
     , intTy
     , intTy
-    , mkFunTys [boolTy] boolTy
+    , mkVisFunTys [boolTy] boolTy
     , boolTy
-    , mkFunTys [intTy, intTy] intTy -- protoypical external function
+    , mkVisFunTys [intTy, intTy] intTy -- protoypical external function
     ]
 
 exprs :: [(String, CoreExpr)]
diff --git a/testsuite/tests/dependent/should_fail/T15215.hs b/testsuite/tests/dependent/should_fail/T15215.hs
index 96fe04385b..e4968a1654 100644
--- a/testsuite/tests/dependent/should_fail/T15215.hs
+++ b/testsuite/tests/dependent/should_fail/T15215.hs
@@ -8,5 +8,9 @@ import Data.Kind
 data A :: Type -> Type where
   MkA :: Show (Maybe a) => A a
 
+data B :: Type -> Type where
+  MkB :: Show a => B a
+
 data SA :: forall a. A a -> Type where
   SMkA :: SA MkA
+  SMkB :: SA MkB
diff --git a/testsuite/tests/dependent/should_fail/T15215.stderr b/testsuite/tests/dependent/should_fail/T15215.stderr
index 53aff765a3..be2d7c75e7 100644
--- a/testsuite/tests/dependent/should_fail/T15215.stderr
+++ b/testsuite/tests/dependent/should_fail/T15215.stderr
@@ -5,8 +5,9 @@ T15215.hs:9:3: error:
     • In the definition of data constructor ‘MkA’
       In the data type declaration for ‘A’
 
-T15215.hs:12:14: error:
-    • Illegal constraint in a kind: Show (Maybe a0)
-    • In the first argument of ‘SA’, namely ‘MkA’
-      In the type ‘SA MkA’
-      In the definition of data constructor ‘SMkA’
+T15215.hs:16:14: error:
+    • Data constructor ‘MkB’ cannot be used here
+        (it has an unpromotable context ‘Show a’)
+    • In the first argument of ‘SA’, namely ‘MkB’
+      In the type ‘SA MkB’
+      In the definition of data constructor ‘SMkB’
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 9c34ed4263..8a885b39a5 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -206,4 +206,3 @@ test('T14887a', normal, compile, [''])
 test('T14847', normal, compile, [''])
 test('T15795', normal, compile, [''])
 test('T15795a', normal, compile, [''])
-
diff --git a/testsuite/tests/typecheck/should_fail/T12102.hs b/testsuite/tests/typecheck/should_fail/T12102.hs
index 6d21fef914..b17c9937c8 100644
--- a/testsuite/tests/typecheck/should_fail/T12102.hs
+++ b/testsuite/tests/typecheck/should_fail/T12102.hs
@@ -1,7 +1,8 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeInType #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
+
 module T12102 where
 
 import Data.Kind
diff --git a/testsuite/tests/typecheck/should_fail/T12102.stderr b/testsuite/tests/typecheck/should_fail/T12102.stderr
deleted file mode 100644
index ea3016b21c..0000000000
--- a/testsuite/tests/typecheck/should_fail/T12102.stderr
+++ /dev/null
@@ -1,6 +0,0 @@
-
-T12102.hs:15:1: error:
-    • Illegal constraint in a kind: forall a.
-                                    (IsTypeLit a ~ 'True) =>
-                                    a -> *
-    • In the data type declaration for ‘T’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index bb7ed96327..1a775d3a7c 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -409,7 +409,7 @@ test('T12063', [expect_broken(12063)], multimod_compile_fail, ['T12063', '-v0'])
 test('T12083a', normal, compile_fail, [''])
 test('T12083b', normal, compile_fail, [''])
 test('T11974b', normal, compile_fail, [''])
-test('T12102', normal, compile_fail, [''])
+test('T12102', normal, compile, [''])
 test('T12151', normal, compile_fail, [''])
 test('T7437', normal, compile_fail, [''])
 test('T12177', normal, compile_fail, [''])