#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: | -------------------------------------+------------------------------------- Comment (by goldfire): Here appears to be a smaller, digestible example: {{{#!hs {-# LANGUAGE TypeFamilies, TypeOperators, DataKinds, PolyKinds, GADTs, ScopedTypeVariables #-} f :: [a] -> [a] f [] = [] f [x] = [x] f (x:y:zs) = g y zs where g _ bs = x : bs type family F (as :: [a]) :: [a] where F '[] = '[] F '[x] = '[x] F (x:y:zs) = G x y zs type family G x a bs where G x _ bs = x : bs data family Sing (x :: k) data instance Sing (x :: [a]) where SNil :: Sing '[] SCons :: Sing a -> Sing as -> Sing (a : as) infixr 5 `SCons` sF :: forall (p :: [a]). Sing p -> Sing (F p :: [a]) sF SNil = SNil sF (SCons x SNil) = SCons x SNil sF ((x :: Sing x) `SCons` y `SCons` zs) = sG y zs where sG :: forall b c. Sing b -> Sing c -> Sing (G x b c) sG _ bs = x `SCons` bs }}} Let's start by examining `f` and `g`, which are ordinary, Haskell98 functions. What's the inferred type of `g`? It depends on whether or not lets are generalized. In Haskell98 (i.e. `NoMonoLocalBinds`), `g` is inferred to have type `forall b. b -> [a] -> [a]`. With `MonoLocalBinds`, `g` is inferred to have type `a -> [a] -> [a]`. Both types allow `f` to type-check, and so the user won't notice this difference. Now let's consider the translation of `f` and `g` to type families. `g` closes over the outer local variable `x`, so we must add `x` to `G`'s parameter list (this is lambda lifting). Note that `F` gets a CUSK, derived from `f`'s type signature. `G` gets no kind annotations, as `g` has no type annotation. GHC infers kind `forall a b. a -> b -> [a] -> [a]` for `G`. Note that, as `G` is not local, its kind is always generalized, regardless of `MonoLocalBinds`. Finally, we consider the singletonized version of `f` and `g`. Note that the type variable bound in `sF`'s type gets a kind signature, as does the result. `sG` gets a type signature, but no variables get kind signatures. (`sG`'s type signature is entirely formulaic, given the singletons pattern.) The only way GHC can figure out the kinds of `b` and `c` is via their usage in the call to `G`. This tells GHC that `c` must have kind `[a]`, but it gives no information about `b`, whose kind remains mysterious. In 8.0, GHC mistakenly quantified over the kind of `b`, leading to `sG :: forall (b :: k) (c :: [a]). ...`. When `sG` is called on `y :: a`, it's specialized with `[k |-> a]` and all is well. However, now that kind generalization is working properly, GHC does ''not'' quantify over `k` and leaves it as a metavariable to be solved. What puzzles me a bit now that I look at this is that `k` should be able to be solved in the no-generalization case: `k` is determined by the call `sG y zs`, where we can see that `k := a` is a good solution. But GHC reports `k` as untouchable at this point.... and I don't know why. There seems to be no equality constraints brought into scope between `sG y zs` and the introduction of `k`, so I don't know why it would be untouchable. I will examine again in due course. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13549#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler