Fix #12442.

The problem is described in the ticket.

This patch adds new variants of the access points to the pure
unifier that allow unification of types only when the caller
wants this behavior. (The unifier used to also unify kinds.)
This behavior is appropriate when the kinds are either already
known to be the same, or the list of types provided are a
list of well-typed arguments to some type constructor. In the
latter case, unifying earlier types in the list will unify the
kinds of any later (dependent) types.

At use sites, I went through and chose the unification function
according to the criteria above.

This patch includes some modest performance improvements as we
are now doing less work.

3 files changed, 64 insertions, 3 deletions

diff --git a/testsuite/tests/dependent/should_compile/T12442.hs b/testsuite/tests/dependent/should_compile/T12442.hs
new file mode 100644
index 0000000000..f9dbf0a486
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T12442.hs
@@ -0,0 +1,57 @@
+-- Based on https://github.com/idris-lang/Idris-dev/blob/v0.9.10/libs/effects/Effects.idr
+
+{-# LANGUAGE TypeInType, ScopedTypeVariables, TypeOperators, TypeApplications,
+             GADTs, TypeFamilies, AllowAmbiguousTypes #-}
+
+module T12442 where
+
+import Data.Kind
+
+data family Sing (a :: k)
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+type family (a :: k1 ~> k2) @@ (b :: k1) :: k2
+
+data TyCon1 :: (Type -> Type) -> (Type ~> Type)
+type instance (TyCon1 t) @@ x = t x
+
+data TyCon2 :: (Type -> Type -> Type) -> (Type ~> Type ~> Type)
+type instance (TyCon2 t) @@ x = (TyCon1 (t x))
+
+data TyCon3 :: (Type -> Type -> Type -> Type) -> (Type ~> Type ~> Type ~> Type)
+type instance (TyCon3 t) @@ x = (TyCon2 (t x))
+
+type Effect = Type ~> Type ~> Type ~> Type
+
+data EFFECT :: Type where
+  MkEff :: Type -> Effect -> EFFECT
+
+data EffElem :: (Type ~> Type ~> Type ~> Type) -> Type -> [EFFECT] -> Type where
+  Here :: EffElem x a (MkEff a x ': xs)
+
+data instance Sing (elem :: EffElem x a xs) where
+  SHere :: Sing Here
+
+type family UpdateResTy b t (xs :: [EFFECT]) (elem :: EffElem e a xs)
+                        (thing :: e @@ a @@ b @@ t) :: [EFFECT] where
+  UpdateResTy b _ (MkEff a e ': xs) Here n = MkEff b e ': xs
+
+data EffM :: (Type ~> Type) -> [EFFECT] -> [EFFECT] -> Type -> Type
+
+effect :: forall e a b t xs prf eff m.
+          Sing (prf :: EffElem e a xs)
+       -> Sing (eff :: e @@ a @@ b @@ t)
+       -> EffM m xs (UpdateResTy b t xs prf eff) t
+effect = undefined
+
+data State :: Type -> Type -> Type -> Type where
+  Get :: State a a a
+
+data instance Sing (e :: State a b c) where
+  SGet :: Sing Get
+
+type STATE t = MkEff t (TyCon3 State)
+
+get_ :: forall m x. EffM m '[STATE x] '[STATE x] x
+get_ = effect @(TyCon3 State) SHere SGet
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 5985fd9fbb..6d39e45000 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -21,3 +21,4 @@ test('T11711', normal, compile, [''])
 test('RaeJobTalk', normal, compile, [''])
 test('T11635', normal, compile, [''])
 test('T11719', normal, compile, [''])
+test('T12442', normal, compile, [''])
diff --git a/testsuite/tests/perf/compiler/all.T b/testsuite/tests/perf/compiler/all.T
index 7594d1914a..f93d8ca4a8 100644
--- a/testsuite/tests/perf/compiler/all.T
+++ b/testsuite/tests/perf/compiler/all.T
@@ -585,7 +585,7 @@ test('T5837',
              # 2014-12-08: 115905208  Constraint solver perf improvements (esp kick-out)
              # 2016-04-06: 24199320  (x86/Linux, 64-bit machine) TypeInType
 
-           (wordsize(64), 48507272, 10)])
+           (wordsize(64), 42445672, 10)])
              # sample: 3926235424 (amd64/Linux, 15/2/2012)
              # 2012-10-02 81879216
              # 2012-09-20 87254264 amd64/Linux
@@ -604,6 +604,7 @@ test('T5837',
              # 2015-12-11 43877520  amd64/Linux, TypeInType (see #11196)
              # 2016-03-18 48507272  Mac, accept small regression in exchange
              #                           for other optimisations
+             # 2016-09-15 42445672  Linux; fixing #12422
       ],
       compile_fail,['-freduction-depth=50'])
 
@@ -715,13 +716,14 @@ test('T9872a',
 test('T9872b',
      [ only_ways(['normal']),
        compiler_stats_num_field('bytes allocated',
-          [(wordsize(64), 4600233488, 5),
+          [(wordsize(64), 4069522928, 5),
           # 2014-12-10    6483306280    Initally created
           # 2014-12-16    6892251912    Flattener parameterized over roles
           # 2014-12-18    3480212048    Reduce type families even more eagerly
           # 2015-12-11    5199926080    TypeInType (see #11196)
           # 2016-02-08    4918990352    Improved a bit by tyConRolesRepresentational
           # 2016-04-06:   4600233488    Refactoring of CSE #11781
+          # 2016-09-15:   4069522928    Fix #12422
            (wordsize(32), 2422750696, 5)
           # was           1700000000
           # 2016-04-06    2422750696    x86/Linux
@@ -732,13 +734,14 @@ test('T9872b',
 test('T9872c',
      [ only_ways(['normal']),
        compiler_stats_num_field('bytes allocated',
-          [(wordsize(64), 4306667256, 5),
+          [(wordsize(64), 3702580928, 5),
           # 2014-12-10    5495850096    Initally created
           # 2014-12-16    5842024784    Flattener parameterized over roles
           # 2014-12-18    2963554096    Reduce type families even more eagerly
           # 2015-12-11    4723613784    TypeInType (see #11196)
           # 2016-02-08    4454071184    Improved a bit by tyConRolesRepresentational
           # 2016-04-06:   4306667256    Refactoring of CSE #11781
+          # 2016-09-15:   3702580928    Fixing #12422
            (wordsize(32), 2257242896, 5)
           # was           1500000000
           # 2016-04-06    2257242896