Put kind variables before type variables when specializing

When you reverse the order of uniques you get the core lint
error from the testcase. The testcase is copied from
tests/simplCore/should_compile/T10689a.hs.

The problem is that we would put type and kind variables ordered by
unique order, which happened to be the right order for this testcase to
pass under normal conditions.

I think it's enough to sort them with `sortQuantVars`, but I'm not
really sure if some more sophisticated dependency analysis isn't needed.

Test Plan: added a new testcase

Reviewers: simonpj, goldfire, simonmar, austin, bgamari

Reviewed By: bgamari

Subscribers: thomie

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

3 files changed, 315 insertions, 0 deletions

diff --git a/testsuite/tests/determinism/should_compile/Makefile b/testsuite/tests/determinism/should_compile/Makefile
new file mode 100644
index 0000000000..9101fbd40a
--- /dev/null
+++ b/testsuite/tests/determinism/should_compile/Makefile
@@ -0,0 +1,3 @@
+TOP=../../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/determinism/should_compile/all.T b/testsuite/tests/determinism/should_compile/all.T
new file mode 100644
index 0000000000..aa7b2fb5b2
--- /dev/null
+++ b/testsuite/tests/determinism/should_compile/all.T
@@ -0,0 +1 @@
+test('determ004', normal, compile, ['-dinitial-unique=8388608 -dunique-increment=-1'])
diff --git a/testsuite/tests/determinism/should_compile/determ004.hs b/testsuite/tests/determinism/should_compile/determ004.hs
new file mode 100644
index 0000000000..c74f8d02d8
--- /dev/null
+++ b/testsuite/tests/determinism/should_compile/determ004.hs
@@ -0,0 +1,311 @@
+{-# LANGUAGE TypeOperators
+           , DataKinds
+           , PolyKinds
+           , TypeFamilies
+           , GADTs
+           , UndecidableInstances
+           , RankNTypes
+           , ScopedTypeVariables
+  #-}
+
+{-# OPTIONS_GHC -Wall #-}
+{-# OPTIONS_GHC -Werror #-}
+{-# OPTIONS_GHC -O1 -fspec-constr #-}
+
+{-
+
+With reversed order of allocated uniques the type variables would be in
+wrong order:
+
+*** Core Lint errors : in result of SpecConstr ***
+determ004.hs:88:12: warning:
+    [in body of lambda with binder m_azbFg :: a_afdP_azbON]
+    @ (a_afdP_azbON :: BOX) is out of scope
+*** Offending Program ***
+
+...
+
+Rec {
+$s$wsFoldr1_szbtK
+  :: forall (m_azbFg :: a_afdP_azbON)
+            (x_azbOM :: TyFun
+                          a_afdP_azbON (TyFun a_afdP_azbON a_afdP_azbON -> *)
+                        -> *)
+            (a_afdP_azbON :: BOX)
+            (ipv_szbwN :: a_afdP_azbON)
+            (ipv_szbwO :: [a_afdP_azbON]).
+     R:Sing[]z (ipv_szbwN : ipv_szbwO)
+     ~R# Sing (Apply (Apply (:$) ipv_szbwN) ipv_szbwO)
+     -> Sing ipv_szbwO
+     -> Sing ipv_szbwN
+     -> (forall (t_azbNM :: a_afdP_azbON).
+         Sing t_azbNM -> Sing (Apply x_azbOM t_azbNM))
+     -> Sing
+          (Apply
+             (Apply Foldr1Sym0 x_azbOM)
+             (Let1627448493XsSym4 x_azbOM m_azbFg ipv_szbwN ipv_szbwO))
+[LclId,
+ Arity=4,
+ Str=DmdType <L,U><L,U><L,U><C(S(C(S))),C(U(1*C1(U)))>]
+$s$wsFoldr1_szbtK =
+  \ (@ (m_azbFg :: a_afdP_azbON))
+    (@ (x_azbOM :: TyFun
+                     a_afdP_azbON (TyFun a_afdP_azbON a_afdP_azbON -> *)
+                   -> *))
+    (@ (a_afdP_azbON :: BOX))
+    (@ (ipv_szbwN :: a_afdP_azbON))
+    (@ (ipv_szbwO :: [a_afdP_azbON]))
+    (sg_szbtL
+       :: R:Sing[]z (ipv_szbwN : ipv_szbwO)
+          ~R# Sing (Apply (Apply (:$) ipv_szbwN) ipv_szbwO))
+    (sc_szbtM :: Sing ipv_szbwO)
+    (sc_szbtN :: Sing ipv_szbwN)
+    (sc_szbtP
+       :: forall (t_azbNM :: a_afdP_azbON).
+          Sing t_azbNM -> Sing (Apply x_azbOM t_azbNM)) ->
+    case (SCons
+            @ a_afdP_azbON
+            @ (ipv_szbwN : ipv_szbwO)
+            @ ipv_szbwO
+            @ ipv_szbwN
+            @~ (<ipv_szbwN : ipv_szbwO>_N
+                :: (ipv_szbwN : ipv_szbwO) ~# (ipv_szbwN : ipv_szbwO))
+            sc_szbtN
+            sc_szbtM)
+         `cast` (sg_szbtL
+                 ; TFCo:R:Sing[]z[0] <a_afdP_azbON>_N <Let1627448493XsSym4
+                                                         x_azbOM m_azbFg ipv_szbwN ipv_szbwO>_N
+                 :: R:Sing[]z (ipv_szbwN : ipv_szbwO)
+                    ~R# R:Sing[]z
+                          (Let1627448493XsSym4 x_azbOM m_azbFg ipv_szbwN ipv_szbwO))
+    of wild_XD {
+      SNil dt_dzbxX ->
+        (lvl_szbwi @ a_afdP_azbON)
+        `cast` ((Sing
+                   (Sym (TFCo:R:Foldr1[2] <a_afdP_azbON>_N <x_azbOM>_N)
+                    ; Sym
+                        (TFCo:R:Apply[]kFoldr1Sym1l_afe2[0]
+                           <a_afdP_azbON>_N <'[]>_N <x_azbOM>_N)
+                    ; (Apply
+                         (Sym
+                            (TFCo:R:Apply(->)(->)Foldr1Sym0l[0] <a_afdP_azbON>_N <x_azbOM>_N))
+                         (Sym dt_dzbxX))_N))_R
+                :: Sing (Apply ErrorSym0 "Data.Singletons.List.foldr1: empty list")
+                   ~R# Sing
+                         (Apply
+                            (Apply Foldr1Sym0 x_azbOM)
+                            (Let1627448493XsSym4 x_azbOM m_azbFg ipv_szbwN ipv_szbwO)));
+      SCons @ n_azbFh @ m_XzbGe dt_dzbxK _sX_azbOH
+            ds_dzbyu [Dmd=<S,1*U>] ->
+        case ds_dzbyu
+             `cast` (TFCo:R:Sing[]z[0] <a_afdP_azbON>_N <n_azbFh>_N
+                     :: Sing n_azbFh ~R# R:Sing[]z n_azbFh)
+        of wild_Xo {
+          SNil dt_dzbxk ->
+            (lvl_szbw1 @ a_afdP_azbON @ m_XzbGe)
+            `cast` ((Sing
+                       (Sym (TFCo:R:Foldr1[0] <a_afdP_azbON>_N <m_XzbGe>_N <x_azbOM>_N)
+                        ; Sym
+                            (TFCo:R:Apply[]kFoldr1Sym1l_afe2[0]
+                               <a_afdP_azbON>_N <'[m_XzbGe]>_N <x_azbOM>_N)
+                        ; (Apply
+                             (Sym
+                                (TFCo:R:Apply(->)(->)Foldr1Sym0l[0] <a_afdP_azbON>_N <x_azbOM>_N))
+                             ((<m_XzbGe>_N ': Sym dt_dzbxk)_N ; Sym dt_dzbxK))_N))_R
+                    :: Sing m_XzbGe
+                       ~R# Sing
+                             (Apply
+                                (Apply Foldr1Sym0 x_azbOM)
+                                (Let1627448493XsSym4 x_azbOM m_azbFg ipv_szbwN ipv_szbwO)));
+          SCons @ ipv_XzbxR @ ipv_XzbyV ipv_szbwM ipv_szbwL ipv_szbwK ->
+            case (sc_szbtP @ m_XzbGe _sX_azbOH)
+                 `cast` (TFCo:R:Sing(->)f[0]
+                           <a_afdP_azbON>_N <a_afdP_azbON>_N <Apply x_azbOM m_XzbGe>_N
+                         :: Sing (Apply x_azbOM m_XzbGe)
+                            ~R# R:Sing(->)f (Apply x_azbOM m_XzbGe))
+            of wild_X3X { SLambda ds_XzbBr [Dmd=<C(S),1*C1(U)>] ->
+            (ds_XzbBr
+               @ (Foldr1 x_azbOM (ipv_XzbyV : ipv_XzbxR))
+               (($wsFoldr1_szbuc
+                   @ a_afdP_azbON
+                   @ x_azbOM
+                   @ (Let1627448493XsSym4 x_azbOM m_XzbGe ipv_XzbyV ipv_XzbxR)
+                   sc_szbtP
+                   ((SCons
+                       @ a_afdP_azbON
+                       @ (ipv_XzbyV : ipv_XzbxR)
+                       @ ipv_XzbxR
+                       @ ipv_XzbyV
+                       @~ (<ipv_XzbyV : ipv_XzbxR>_N
+                           :: (ipv_XzbyV : ipv_XzbxR) ~# (ipv_XzbyV : ipv_XzbxR))
+                       ipv_szbwL
+                       ipv_szbwK)
+                    `cast` (Sym (TFCo:R:Sing[]z[0] <a_afdP_azbON>_N) (Sym
+                                                                        (TFCo:R:Apply[][]:$$i[0]
+                                                                           <a_afdP_azbON>_N
+                                                                           <ipv_XzbxR>_N
+                                                                           <ipv_XzbyV>_N)
+                                                                      ; (Apply
+                                                                           (Sym
+                                                                              (TFCo:R:Applyk(->):$l[0]
+                                                                                 <a_afdP_azbON>_N
+                                                                                 <ipv_XzbyV>_N))
+                                                                           <ipv_XzbxR>_N)_N)
+                            :: R:Sing[]z (ipv_XzbyV : ipv_XzbxR)
+                               ~R# Sing (Apply (Apply (:$) ipv_XzbyV) ipv_XzbxR))))
+                `cast` ((Sing
+                           ((Apply
+                               (TFCo:R:Apply(->)(->)Foldr1Sym0l[0] <a_afdP_azbON>_N <x_azbOM>_N)
+                               <Let1627448493XsSym4 x_azbOM m_XzbGe ipv_XzbyV ipv_XzbxR>_N)_N
+                            ; TFCo:R:Apply[]kFoldr1Sym1l_afe2[0]
+                                <a_afdP_azbON>_N
+                                ((Apply
+                                    (TFCo:R:Applyk(->):$l[0] <a_afdP_azbON>_N <ipv_XzbyV>_N)
+                                    <ipv_XzbxR>_N)_N
+                                 ; TFCo:R:Apply[][]:$$i[0]
+                                     <a_afdP_azbON>_N <ipv_XzbxR>_N <ipv_XzbyV>_N)
+                                <x_azbOM>_N))_R
+                        :: Sing
+                             (Apply
+                                (Apply Foldr1Sym0 x_azbOM)
+                                (Let1627448493XsSym4 x_azbOM m_XzbGe ipv_XzbyV ipv_XzbxR))
+                           ~R# Sing (Foldr1Sym2 x_azbOM (ipv_XzbyV : ipv_XzbxR)))))
+            `cast` ((Sing
+                       ((Apply
+                           <Apply x_azbOM m_XzbGe>_N
+                           (Sym
+                              (TFCo:R:Apply[]kFoldr1Sym1l_afe2[0]
+                                 <a_afdP_azbON>_N <ipv_XzbyV : ipv_XzbxR>_N <x_azbOM>_N)
+                            ; (Apply
+                                 (Sym
+                                    (TFCo:R:Apply(->)(->)Foldr1Sym0l[0]
+                                       <a_afdP_azbON>_N <x_azbOM>_N))
+                                 (Sym
+                                    (TFCo:R:Apply[][]:$$i[0]
+                                       <a_afdP_azbON>_N <ipv_XzbxR>_N <ipv_XzbyV>_N)
+                                  ; (Apply
+                                       (Sym
+                                          (TFCo:R:Applyk(->):$l[0] <a_afdP_azbON>_N <ipv_XzbyV>_N))
+                                       <ipv_XzbxR>_N)_N))_N))_N
+                        ; Sym
+                            (TFCo:R:Foldr1[1]
+                               <a_afdP_azbON>_N
+                               <ipv_XzbxR>_N
+                               <ipv_XzbyV>_N
+                               <m_XzbGe>_N
+                               <x_azbOM>_N)
+                        ; Sym
+                            (TFCo:R:Apply[]kFoldr1Sym1l_afe2[0]
+                               <a_afdP_azbON>_N <m_XzbGe : ipv_XzbyV : ipv_XzbxR>_N <x_azbOM>_N)
+                        ; (Apply
+                             (Sym
+                                (TFCo:R:Apply(->)(->)Foldr1Sym0l[0] <a_afdP_azbON>_N <x_azbOM>_N))
+                             ((<m_XzbGe>_N ': Sym ipv_szbwM)_N ; Sym dt_dzbxK))_N))_R
+                    :: Sing
+                         (Apply
+                            (Apply x_azbOM m_XzbGe)
+                            (Foldr1Sym2 x_azbOM (ipv_XzbyV : ipv_XzbxR)))
+                       ~R# Sing
+                             (Apply
+                                (Apply Foldr1Sym0 x_azbOM)
+                                (Let1627448493XsSym4 x_azbOM m_azbFg ipv_szbwN ipv_szbwO)))
+            }
+        }
+    }
+...
+-}
+
+module List (sFoldr1) where
+
+data Proxy t
+
+data family Sing (a :: k)
+
+data TyFun (a :: *) (b :: *)
+
+type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2
+
+data instance Sing (f :: TyFun k1 k2 -> *) =
+  SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }
+
+type SingFunction1 f = forall t. Sing t -> Sing (Apply f t)
+
+type SingFunction2 f = forall t. Sing t -> SingFunction1 (Apply f t)
+singFun2 :: Proxy f -> SingFunction2 f -> Sing f
+singFun2 _ f = SLambda (\x -> SLambda (f x))
+
+data (:$$) (j :: a) (i :: TyFun [a] [a])
+type instance Apply ((:$$) j) i = (:) j i
+
+data (:$) (l :: TyFun a (TyFun [a] [a] -> *))
+type instance Apply (:$) l = (:$$) l
+data instance Sing (z :: [a])
+  = z ~ '[] =>
+    SNil
+  | forall (m :: a)
+           (n :: [a]). z ~ (:) m n =>
+    SCons (Sing m) (Sing n)
+
+data ErrorSym0 (t1 :: TyFun k1 k2)
+
+type Let1627448493XsSym4 t_afee t_afef t_afeg t_afeh = Let1627448493Xs t_afee t_afef t_afeg t_afeh
+
+type Let1627448493Xs f_afe9
+                     x_afea
+                     wild_1627448474_afeb
+                     wild_1627448476_afec =
+    Apply (Apply (:$) wild_1627448474_afeb) wild_1627448476_afec
+type Foldr1Sym2 (t_afdY :: TyFun a_afdP (TyFun a_afdP a_afdP -> *)
+                           -> *)
+                (t_afdZ :: [a_afdP]) =
+    Foldr1 t_afdY t_afdZ
+data Foldr1Sym1 (l_afe3 :: TyFun a_afdP (TyFun a_afdP a_afdP -> *)
+                           -> *)
+                (l_afe2 :: TyFun [a_afdP] a_afdP)
+type instance Apply (Foldr1Sym1 l_afe3) l_afe2 = Foldr1Sym2 l_afe3 l_afe2
+
+data Foldr1Sym0 (l_afe0 :: TyFun (TyFun a_afdP (TyFun a_afdP a_afdP
+                                                -> *)
+                                  -> *) (TyFun [a_afdP] a_afdP -> *))
+type instance Apply Foldr1Sym0 l = Foldr1Sym1 l
+
+type family Foldr1 (a_afe5 :: TyFun a_afdP (TyFun a_afdP a_afdP
+                                            -> *)
+                              -> *)
+                   (a_afe6 :: [a_afdP]) :: a_afdP where
+  Foldr1 z_afe7 '[x_afe8] = x_afe8
+  Foldr1 f_afe9 ((:) x_afea ((:) wild_1627448474_afeb wild_1627448476_afec)) = Apply (Apply f_afe9 x_afea) (Apply (Apply Foldr1Sym0 f_afe9) (Let1627448493XsSym4 f_afe9 x_afea wild_1627448474_afeb wild_1627448476_afec))
+  Foldr1 z_afew '[] = Apply ErrorSym0 "Data.Singletons.List.foldr1: empty list"
+
+sFoldr1 ::
+  forall (x :: TyFun a_afdP (TyFun a_afdP a_afdP -> *) -> *)
+         (y :: [a_afdP]).
+  Sing x
+  -> Sing y -> Sing (Apply (Apply Foldr1Sym0 x) y)
+sFoldr1 _ (SCons _sX SNil) = undefined
+sFoldr1 sF (SCons sX (SCons sWild_1627448474 sWild_1627448476))
+  = let
+      lambda_afeC ::
+        forall f_afe9 x_afea wild_1627448474_afeb wild_1627448476_afec.
+        Sing f_afe9
+        -> Sing x_afea
+           -> Sing wild_1627448474_afeb
+              -> Sing wild_1627448476_afec
+                 -> Sing (Apply (Apply Foldr1Sym0 f_afe9) (Apply (Apply (:$) x_afea) (Apply (Apply (:$) wild_1627448474_afeb) wild_1627448476_afec)))
+      lambda_afeC f_afeD x_afeE wild_1627448474_afeF wild_1627448476_afeG
+        = let
+            sXs ::
+              Sing (Let1627448493XsSym4 f_afe9 x_afea wild_1627448474_afeb wild_1627448476_afec)
+            sXs
+              = applySing
+                  (applySing
+                     (singFun2 (undefined :: Proxy (:$)) SCons) wild_1627448474_afeF)
+                  wild_1627448476_afeG
+          in
+            applySing
+              (applySing f_afeD x_afeE)
+              (applySing
+                 (applySing (singFun2 (undefined :: Proxy Foldr1Sym0) sFoldr1) f_afeD)
+                 sXs)
+    in lambda_afeC sF sX sWild_1627448474 sWild_1627448476
+sFoldr1 _ SNil = undefined