[GHC] #13549: GHC 8.2.1's typechecker rejects code generated by singletons that 8.0 accepts

[GHC]

#13549: GHC 8.2.1's typechecker rejects code generated by singletons that 8.0
accepts
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:  8.4.1
       Component:  Compiler (Type    |              Version:  8.1
  checker)                           |
      Resolution:  duplicate         |             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:                    |
-------------------------------------+-------------------------------------
Changes (by goldfire):

 * status:  new => closed
 * resolution:   => duplicate


Comment:

 I think I understand this now. This is a fundamental difference between
 inference for types and inference for kinds.

 Here is the original, unsingletonized code in question:

 {{{#!hs
 permutations            :: [a] -> [[a]]
 permutations xs0        =  xs0 : perms xs0 []
   where
     -- perms :: forall a. [a] -> [a] -> [[a]]
     perms []     _  = []
     perms (t:ts) is = foldr interleave (perms ts (t:is)) (permutations is)
       where -- interleave :: [a] -> [[a]] -> [[a]]
             interleave    xs     r = let (_,zs) = interleave' id xs r in
 zs

             -- interleave' :: ([a] -> [a]) -> [a] -> [[a]] -> ([a],[[a]])
             interleave' _ []     r = (ts, r)
             interleave' f (y:ys) r = let (us,zs) = interleave' (f . (y:))
 ys r
                                      in  (y:us, f (t:y:us) : zs)
 }}}

 Note that the local function signatures are commented out. This code
 compiles, although if you uncomment the type signatures, you'd need
 `ScopedTypeVariables`.

 Let's consider type-checking this with `MonoLocalBinds` on (that is, "let
 should not be generalized"). The body of `interleave'` mentions `t`, a
 variable that's not local to `interleave'`. Thus, according to
 `MonoLocalBinds`, its type should not be generalized. The problem is that
 the type cannot be fully figured out solely by looking at the definition
 of `interleave'`: by the time type inference is done with `interleave'`,
 we know only that its type looks like `([a1] -> a2) -> [a1] -> [a2] ->
 ([a1], [a2])`. Later, we will learn that `a2` is really `[a1]`. This is
 just fine for type inference, but it's bad for kind inference.

 The problem is that when GHC sees a type signature `x :: ty`, it
 interprets `ty` independent of any definition or usage of `x`. After
 processing that statement, `ty` has been desugared and is set in stone --
 including the kinds of any type variables in `ty`.

 After singletonizing, the type of the singletonized version of
 `interleave'` will mention the type family `Interleave'`, whose body is
 just like that of `interleave'`. This type family's kind ''will'' mention
 both `a1` and `a2`, as it has no reason not to. So `sInterleave'` would
 also have to have a generalized kind for it all to work out. But with the
 improvement in `decideKindGeneralisationPlan`, this doesn't happen.

 So, here is the characterization of the infelicity in singletons: if a
 local function's type would be different depending on the presence of
 `MonoLocalBinds`, then it needs a type signature in order for singletons
 to work. In the case of `interleave'`, without `MonoLocalBinds`, `a2` is
 quantified over, leading to a different type than it would have otherwise.
 (Note that the kind for the `Interleave'` type family is generalized,
 regardless of `MonoLocalBinds`.)

 I'm fairly confident in this analysis. I'm going to close the ticket as a
 dup of #13555.

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