[GHC] #15472: GHC HEAD type inference regression post-"Remove decideKindGeneralisationPlan"

[GHC]

#15472: GHC HEAD type inference regression post-"Remove
decideKindGeneralisationPlan"
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.8.1
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 This is subtle, but I claim that the new behavior is correct. I don't know
 what disaster that spells for `singletons`. By the way, I hate CUSKs.

 Here is what's happening.

 1. `LetInterleave` gets the kind `forall (k1 :: Type) (k2 :: Type) (k3 ::
 Type) (k4 :: Type) (a :: Type). k1 -> k2 -> k3 -> k4 -> [a] -> [[a]] ->
 [[a]]`  (ignoring the fact that type families must be saturated / don't
 have kinds, which is not at issue here).

 2. `LetInterleaveSym4` doesn't constrain any of its type variables. We
 thus have `LetInterleaveSym4 :: forall (k1 :: Type) (k2 :: Type) (k3 ::
 Type) (k4 :: Type). k1 -> k2 -> k3 -> k4 -> forall (a :: Type). [a] ~>
 [[a]] ~> [[a]]`.

 3. `LetPerms` and `Permutations` are mutually recursive.

 4. But `Permutations` has a CUSK, so its kind is determined before ever
 looking at `LetPerms`. We assign `Permutations :: forall (a :: Type). [a]
 -> [[a]]`.

 5. We then kind-check `LetPerms`. The first argument to `LetPerms`, namely
 `xs0`, is unconstrained by any pattern or usage. We thus infer `LetPerms
 :: forall (k :: Type) (a :: Type). k -> [a] -> [a] -> [[a]]`.

 6. We process the type signature for `sPermutations`, getting
 `sPermutations :: forall (a :: Type) (t1 :: [a]). Sing t1 -> Sing
 (Permutations t1)`.

 7. `a` and `t1` are brought into scope (via `ScopedTypeVariables`) in the
 definition of `sPermutations`.

 8. We process the type signature for `sPerms`. According to the lack of
 `decideKindGeneralisationPlan`, we then ''generalize'' this type. We get
 `sPerms :: forall (a2 :: Type) (arg1 :: [a2]) (arg2 :: [a2]). Sing arg1 ->
 Sing arg2 -> Sing (LetPerms xs0 arg1 arg2)`. Note that nothing tells us
 that the `a2` in the kind of `arg1` and `arg2` should be the same as `a`.

 9. The patterns for the second equation of `sPerms` bring type variables
 into scope as follows: `(t :: a2)`, `(ts :: [a2])`, and `(is :: [a2])`.

 10. We process the type signature for `sInterleave`, getting `sInterleave
 :: forall (t2 :: [a]) (t3 :: [a]). Sing t2 -> Sing t3 -> Sing
 (LetInterleave xs0 t ts is t2 t3)`. This is well-kinded.

 11. We see that `singFun2 :: forall {k1 :: Type} {k2 :: Type} {k3 :: Type}
 (f :: k1 ~> k2 ~> k3). (forall (t1 :: k1). Sing t1 -> forall (t2 :: k2).
 Sing t2 -> Sing (f @@ t1 @@ t2)) -> Sing f`.

 12. We can see that `LetInterleaveSym4 xs0 t ts is` has kind `forall b.
 [b] ~> [[b]] ~> [[b]]`.

 13. Thus, we can find the type of `singFun2 @(LetInterleaveSym4 xs0 t ts
 is)` to be `(forall (t1 :: [b0]). Sing t1 -> forall (t2 :: [[b0]]). Sing
 t2 -> Sing (LetInterleaveSym4 xs0 t ts is @@ t1 @@ t2)) -> Sing
 (LetInterleaveSym4 xs0 t ts is)`, where `b0` is a fresh unification
 variable.

 14. We are now checking `sInterleave` against the type `forall (t1 ::
 [b0]). Sing t1 -> forall (t2 :: [[b0]]). Sing t2 -> Sing
 (LetInterleaveSym4 xs0 t ts is @@ t1 @@ t2)`. This works fine, choosing
 `b0` to be `a` (as forced by `sInterleave`'s type signature).

 15. We thus get that `singFun2 @(LetInterleaveSym4 xs0 t ts is)
 sInterleave :: Sing (LetInterleaveSym4 xs0 t ts is @a)`, where I've
 explicitly instantiated the `a` in the return kind of `LetInterleaveSym4`.

 16. We see that `sFoldr :: forall (a :: Type) (b :: Type) (t1 :: a ~> b ~>
 b) (t2 :: b) (t3 :: [a]). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Foldr t1
 t2 t3)`.

 17. From the type of the first argument to `sFoldr`, we see that `t1` must
 instantiate to `LetInterleaveSym4 xs0 t ts is @a :: [a] ~> [[a]] ~>
 [[a]]`.

 18. Thus, the return type of the call to `sFoldr` must be `Sing (Foldr
 (LetInterleaveSym4 xs0 t ts is @a) jibber jabber)`, where `Foldr
 (LetInterleaveSym4 xs0 t ts is @a) jibber jabber :: [[a]]`.

 19. The expected return type of `sPerms` is `Sing (LetPerms xs0 arg1
 arg2)`, where `LetPerms xs0 arg1 arg2 :: [[a2]]`.

 20. We check the return type of `sFoldr` against the expected return type
 of `sPerms` and get a kind error, saying that `a2` doesn't equal `a`.

 (The actual error reported is a type error that gives rise to the kind
 error; GHC reports the type error thinking that types are friendlier than
 kinds.)

 As we can see now, the problem is in the generalization in step 8. But
 this generalization is correct -- that type signature for `sPerms` really
 ''is'' too polymorphic for this usage. Note that this doesn't bite in the
 original, unsingletonized code because there is no signature at all on
 `perms`.

 Possible ways forward for `singletons`:

 A. When the user omits a type signature, make sure that we write a
 ''partial'' type signature (say, by writing `forall (arg1 :: _) (arg2 ::
 _). ...`). Partial type signatures do not get generalized, as doing so
 would be silly.

 B. Give `perms` a type annotation in the original.

 C. Interestingly, don't give `Permutations` a CUSK. If GHC has to do
 mutual kind inference, it discovers that `LetPerms :: [a] -> [a] -> [a] ->
 [[a]]` which then gently guides inference later to be correct. (If you try
 loading this code into GHC 8.4, you discover this less general type for
 `LetPerms`, because the feature that GHC removes types with CUSKs from a
 mutually recursive group is new.)

 Well, that was my mental calisthenics for the day.

 If you agree that this isn't GHC's fault, please close the ticket. Thanks.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15472#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler