#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