[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:                    |
-------------------------------------+-------------------------------------

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