[GHC] #13549: GHC 8.2.1's typechecker rejects code generated by singletons that 8.0 accepts
GHC
ghc-devs at haskell.org
Tue Apr 25 14:20:59 UTC 2017
#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
More information about the ghc-tickets
mailing list