[GHC] #15472: GHC HEAD type inference regression post-"Remove decideKindGeneralisationPlan"
#15472: GHC HEAD type inference regression post-"Remove decideKindGeneralisationPlan" -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.8.1 Component: Compiler | Version: 8.5 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Commit c955a514f033a12f6d0ab0fbacec3e18a5757ab5 (`Remove decideKindGeneralisationPlan`) causes the `singletons` library to no longer compile. Here is as minimal of an example as I can muster: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module Bug (sPermutations) where import Data.Kind data TyFun :: Type -> Type -> Type type a ~> b = TyFun a b -> Type infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 data family Sing :: forall k. k -> Type data instance Sing :: forall a. [a] -> Type where SNil :: Sing '[] SCons :: Sing x -> Sing xs -> Sing (x:xs) newtype instance Sing (f :: k1 ~> k2) = SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) } type SingFunction1 f = forall t. Sing t -> Sing (Apply f t) singFun1 :: forall f. SingFunction1 f -> Sing f singFun1 f = SLambda f type SingFunction2 f = forall t. Sing t -> SingFunction1 (Apply f t) singFun2 :: forall f. SingFunction2 f -> Sing f singFun2 f = SLambda (\x -> singFun1 (f x)) type family Undefined :: k where {} sUndefined :: a sUndefined = undefined type family LetGo k z x ys where LetGo k z x '[] = z LetGo k z x (y ': ys) = Apply (Apply k y) (LetGo k z x ys) type family Foldr (k :: a ~> b ~> b) (x :: b) (xs :: [a]) :: b where Foldr k z x = LetGo k z x x sFoldr :: forall (t1 :: a ~> b ~> b) (t2 :: b) (t3 :: [a]). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Foldr t1 t2 t3 :: b) sFoldr (sK :: Sing k) (sZ :: Sing z) (sX :: Sing x) = let sGo :: forall arg. Sing arg -> Sing (LetGo k z x arg) sGo SNil = sZ sGo (SCons (sY :: Sing y) (sYs :: Sing ys)) = sK `applySing` sY `applySing` sGo sYs in sGo sX type family LetInterleave xs0 t ts is (a1 :: [a]) (a2 :: [[a]]) :: [[a]] where LetInterleave xs0 t ts is a1 a2 = Undefined a1 a2 data LetInterleaveSym5 l_ahko l_ahkp l_ahkq l_ahkr (l_ahks :: [a]) :: [[a]] ~> [[a]] type instance Apply (LetInterleaveSym5 l_ahko l_ahkp l_ahkq l_ahkr l_ahks) l_ahkn = LetInterleave l_ahko l_ahkp l_ahkq l_ahkr l_ahks l_ahkn data LetInterleaveSym4 l_ahkv l_ahkw l_ahkx l_ahky :: forall a. [a] ~> [[a]] ~> [[a]] type instance Apply (LetInterleaveSym4 l_ahkv l_ahkw l_ahkx l_ahky) l_ahku = LetInterleaveSym5 l_ahkv l_ahkw l_ahkx l_ahky l_ahku data LetInterleaveSym3 l_ahkB l_ahkC l_ahkD l_ahkA type instance Apply (LetInterleaveSym3 l_ahkB l_ahkC l_ahkD) l_ahkA = LetInterleaveSym4 l_ahkB l_ahkC l_ahkD l_ahkA data LetInterleaveSym2 l_ahkG l_ahkH l_ahkF type instance Apply (LetInterleaveSym2 l_ahkG l_ahkH) l_ahkF = LetInterleaveSym3 l_ahkG l_ahkH l_ahkF data LetInterleaveSym1 l_ahkK l_ahkJ type instance Apply (LetInterleaveSym1 l_ahkK) l_ahkJ = LetInterleaveSym2 l_ahkK l_ahkJ data LetInterleaveSym0 l_ahkM type instance Apply LetInterleaveSym0 l_ahkM = LetInterleaveSym1 l_ahkM type family LetPerms xs0 a1 a2 where LetPerms xs0 '[] _ = '[] LetPerms xs0 (t ': ts) is = Foldr (LetInterleaveSym4 xs0 t ts is) (LetPerms xs0 ts (t ': is)) (Permutations is) {- $(singletons [d| permutations :: forall a. [a] -> [[a]] permutations xs0 = xs0 : perms xs0 [] where perms [] _ = [] perms (t:ts) is = foldr interleave (perms ts (t:is)) (permutations is) where interleave :: [a] -> [[a]] -> [[a]] interleave = undefined |]) -} type family Permutations (xs0 :: [a]) :: [[a]] where Permutations xs0 = xs0 ': LetPerms xs0 xs0 '[] sPermutations :: forall (t1 :: [a]). Sing t1 -> Sing (Permutations t1 :: [[a]]) sPermutations (sXs0 :: Sing xs0) = let sPerms :: forall arg1 arg2. Sing arg1 -> Sing arg2 -> Sing (LetPerms xs0 arg1 arg2) sPerms SNil _ = SNil sPerms (SCons (sT :: Sing t) (sTs :: Sing ts)) (sIs :: Sing is) = let sInterleave :: forall (t2 :: [a]) (t3 :: [[a]]). Sing t2 -> Sing t3 -> Sing (LetInterleave xs0 t ts is t2 t3 :: [[a]]) sInterleave (sA1 :: Sing a1) (sA2 :: Sing a2) = sUndefined sA1 sA2 in sFoldr (singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave) (sPerms sTs (sT `SCons` sIs)) (sPermutations sIs) in sXs0 `SCons` sPerms sXs0 SNil }}} After that commit, this program (which previously typechecked) now errors with: {{{ $ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:105:66: error: • Could not deduce: t2 ~~ t30 from the context: arg1 ~ (x : xs) bound by a pattern with constructor: SCons :: forall a (x :: a) (xs :: [a]). Sing x -> Sing xs -> Sing (x : xs), in an equation for ‘sPerms’ at Bug.hs:99:17-53 ‘t2’ is a rigid type variable bound by a type expected by the context: SingFunction2 (LetInterleaveSym4 t1 x xs arg2) at Bug.hs:105:24-76 Expected type: Sing t -> Sing t2 -> Sing (Apply (Apply (LetInterleaveSym4 t1 x xs arg2) t) t2) Actual type: Sing t20 -> Sing t30 -> Sing (LetInterleave t1 x xs arg2 t20 t30) • In the second argument of ‘singFun2’, namely ‘sInterleave’ In the first argument of ‘sFoldr’, namely ‘(singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave)’ In the expression: sFoldr (singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave) (sPerms sTs (sT `SCons` sIs)) (sPermutations sIs) • Relevant bindings include sInterleave :: forall (t2 :: [a1]) (t3 :: [[a1]]). Sing t2 -> Sing t3 -> Sing (LetInterleave t1 x xs arg2 t2 t3) (bound at Bug.hs:103:17) sIs :: Sing arg2 (bound at Bug.hs:99:57) sTs :: Sing xs (bound at Bug.hs:99:39) sT :: Sing x (bound at Bug.hs:99:24) sPerms :: Sing arg1 -> Sing arg2 -> Sing (LetPerms t1 arg1 arg2) (bound at Bug.hs:98:9) sXs0 :: Sing t1 (bound at Bug.hs:94:16) (Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max- relevant-binds) | 105 | in sFoldr (singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave) | ^^^^^^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15472 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15472: GHC HEAD type inference regression post-"Remove decideKindGeneralisationPlan" -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: | 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 RyanGlScott): * keywords: => TypeInType * failure: None/Unknown => GHC rejects valid program * component: Compiler => Compiler (Type checker) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15472#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15472: GHC HEAD type inference regression post-"Remove decideKindGeneralisationPlan" -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: | 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): This is subtle, but I claim that the new behavior is correct. I don't know what disaster that spells for `singletons`. By the way, I hate CUSKs. Here is what's happening. 1. `LetInterleave` gets the kind `forall (k1 :: Type) (k2 :: Type) (k3 :: Type) (k4 :: Type) (a :: Type). k1 -> k2 -> k3 -> k4 -> [a] -> [[a]] -> [[a]]` (ignoring the fact that type families must be saturated / don't have kinds, which is not at issue here). 2. `LetInterleaveSym4` doesn't constrain any of its type variables. We thus have `LetInterleaveSym4 :: forall (k1 :: Type) (k2 :: Type) (k3 :: Type) (k4 :: Type). k1 -> k2 -> k3 -> k4 -> forall (a :: Type). [a] ~> [[a]] ~> [[a]]`. 3. `LetPerms` and `Permutations` are mutually recursive. 4. But `Permutations` has a CUSK, so its kind is determined before ever looking at `LetPerms`. We assign `Permutations :: forall (a :: Type). [a] -> [[a]]`. 5. We then kind-check `LetPerms`. The first argument to `LetPerms`, namely `xs0`, is unconstrained by any pattern or usage. We thus infer `LetPerms :: forall (k :: Type) (a :: Type). k -> [a] -> [a] -> [[a]]`. 6. We process the type signature for `sPermutations`, getting `sPermutations :: forall (a :: Type) (t1 :: [a]). Sing t1 -> Sing (Permutations t1)`. 7. `a` and `t1` are brought into scope (via `ScopedTypeVariables`) in the definition of `sPermutations`. 8. We process the type signature for `sPerms`. According to the lack of `decideKindGeneralisationPlan`, we then ''generalize'' this type. We get `sPerms :: forall (a2 :: Type) (arg1 :: [a2]) (arg2 :: [a2]). Sing arg1 -> Sing arg2 -> Sing (LetPerms xs0 arg1 arg2)`. Note that nothing tells us that the `a2` in the kind of `arg1` and `arg2` should be the same as `a`. 9. The patterns for the second equation of `sPerms` bring type variables into scope as follows: `(t :: a2)`, `(ts :: [a2])`, and `(is :: [a2])`. 10. We process the type signature for `sInterleave`, getting `sInterleave :: forall (t2 :: [a]) (t3 :: [a]). Sing t2 -> Sing t3 -> Sing (LetInterleave xs0 t ts is t2 t3)`. This is well-kinded. 11. We see that `singFun2 :: forall {k1 :: Type} {k2 :: Type} {k3 :: Type} (f :: k1 ~> k2 ~> k3). (forall (t1 :: k1). Sing t1 -> forall (t2 :: k2). Sing t2 -> Sing (f @@ t1 @@ t2)) -> Sing f`. 12. We can see that `LetInterleaveSym4 xs0 t ts is` has kind `forall b. [b] ~> [[b]] ~> [[b]]`. 13. Thus, we can find the type of `singFun2 @(LetInterleaveSym4 xs0 t ts is)` to be `(forall (t1 :: [b0]). Sing t1 -> forall (t2 :: [[b0]]). Sing t2 -> Sing (LetInterleaveSym4 xs0 t ts is @@ t1 @@ t2)) -> Sing (LetInterleaveSym4 xs0 t ts is)`, where `b0` is a fresh unification variable. 14. We are now checking `sInterleave` against the type `forall (t1 :: [b0]). Sing t1 -> forall (t2 :: [[b0]]). Sing t2 -> Sing (LetInterleaveSym4 xs0 t ts is @@ t1 @@ t2)`. This works fine, choosing `b0` to be `a` (as forced by `sInterleave`'s type signature). 15. We thus get that `singFun2 @(LetInterleaveSym4 xs0 t ts is) sInterleave :: Sing (LetInterleaveSym4 xs0 t ts is @a)`, where I've explicitly instantiated the `a` in the return kind of `LetInterleaveSym4`. 16. We see that `sFoldr :: forall (a :: Type) (b :: Type) (t1 :: a ~> b ~> b) (t2 :: b) (t3 :: [a]). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Foldr t1 t2 t3)`. 17. From the type of the first argument to `sFoldr`, we see that `t1` must instantiate to `LetInterleaveSym4 xs0 t ts is @a :: [a] ~> [[a]] ~> [[a]]`. 18. Thus, the return type of the call to `sFoldr` must be `Sing (Foldr (LetInterleaveSym4 xs0 t ts is @a) jibber jabber)`, where `Foldr (LetInterleaveSym4 xs0 t ts is @a) jibber jabber :: [[a]]`. 19. The expected return type of `sPerms` is `Sing (LetPerms xs0 arg1 arg2)`, where `LetPerms xs0 arg1 arg2 :: [[a2]]`. 20. We check the return type of `sFoldr` against the expected return type of `sPerms` and get a kind error, saying that `a2` doesn't equal `a`. (The actual error reported is a type error that gives rise to the kind error; GHC reports the type error thinking that types are friendlier than kinds.) As we can see now, the problem is in the generalization in step 8. But this generalization is correct -- that type signature for `sPerms` really ''is'' too polymorphic for this usage. Note that this doesn't bite in the original, unsingletonized code because there is no signature at all on `perms`. Possible ways forward for `singletons`: A. When the user omits a type signature, make sure that we write a ''partial'' type signature (say, by writing `forall (arg1 :: _) (arg2 :: _). ...`). Partial type signatures do not get generalized, as doing so would be silly. B. Give `perms` a type annotation in the original. C. Interestingly, don't give `Permutations` a CUSK. If GHC has to do mutual kind inference, it discovers that `LetPerms :: [a] -> [a] -> [a] -> [[a]]` which then gently guides inference later to be correct. (If you try loading this code into GHC 8.4, you discover this less general type for `LetPerms`, because the feature that GHC removes types with CUSKs from a mutually recursive group is new.) Well, that was my mental calisthenics for the day. If you agree that this isn't GHC's fault, please close the ticket. Thanks. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15472#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15472: GHC HEAD type inference regression post-"Remove decideKindGeneralisationPlan" -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: highest | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: invalid | 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 RyanGlScott): * status: new => closed * resolution: => invalid Comment: Thanks, goldfire! I am quite appreciative of the time you took to make that very detailed response. If you're convinced that this is correct behavior, then I'm convinced too, so I'll close this. Fortunately, `singletons` doesn't have to work very hard at all to work around this. Option (B) does indeed work quite nicely (and is backwards compatible): {{{#!diff diff -ru singletons-2.4.1.orig/src/Data/Singletons/Prelude/List.hs singletons-2.4.1/src/Data/Singletons/Prelude/List.hs --- singletons-2.4.1.orig/src/Data/Singletons/Prelude/List.hs 2018-01-08 11:09:19.000000000 -0500 +++ singletons-2.4.1/src/Data/Singletons/Prelude/List.hs 2018-08-03 12:53:25.480813967 -0400 @@ -310,6 +310,7 @@ permutations :: forall a. [a] -> [[a]] permutations xs0 = xs0 : perms xs0 [] where + perms :: [a] -> [a] -> [[a]] perms [] _ = [] perms (t:ts) is = foldr interleave (perms ts (t:is)) (permutations is) where interleave xs r = let (_,zs) = interleave' id xs r in zs }}} An alternative option (D) is to leave off the type signature for `interleave` entirely. (Unfortunately, that's not backwards compatible due to #13549/#13555, but //c'est la vie//.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15472#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15472: GHC HEAD type inference regression post-"Remove decideKindGeneralisationPlan" -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: highest | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: invalid | 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 monoidal): Is there a small program that would demonstrate the difference in behavior? Might be worth adding to the testsuite. Or is this already covered by existing tests? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15472#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15472: GHC HEAD type inference regression post-"Remove decideKindGeneralisationPlan" -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: highest | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: invalid | 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 RyanGlScott): If you can successfully find a smaller program than this which exhibits the same issue, then I applaud you. But the original program is small enough that it may be worth checking in under a `should_fail` directory somewhere in the test suite. Also, we should mention this in the GHC 8.8 migration guide (https://ghc.haskell.org/trac/ghc/wiki/Status/GHC-8.8.1). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15472#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15472: GHC HEAD type inference regression post-"Remove decideKindGeneralisationPlan" -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: highest | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: invalid | 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 RyanGlScott): Actually, here is an ever-so-slightly smaller way to trigger the issue (which I also discovered in `singletons`) {{{#!hs {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module Bug where import Data.Kind import Data.List.NonEmpty (NonEmpty(..)) data TyFun :: Type -> Type -> Type type a ~> b = TyFun a b -> Type infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 data family Sing :: forall k. k -> Type data instance Sing :: forall a. [a] -> Type where SNil :: Sing '[] SCons :: Sing x -> Sing xs -> Sing (x:xs) data instance Sing :: forall a. NonEmpty a -> Type where (:%|) :: Sing x -> Sing xs -> Sing (x :| xs) type family LetGo x xs b cs where LetGo x xs b (c:cs) = b <> LetGo x xs c cs LetGo x xs b '[] = b type family SconcatDefault (arg :: NonEmpty a) :: a where SconcatDefault (x :| xs) = LetGo x xs x xs class PSemigroup (a :: Type) where type (<>) (arg1 :: a) (arg2 :: a) :: a type Sconcat (arg :: NonEmpty a) :: a type Sconcat arg = SconcatDefault arg class SSemigroup a where (%<>) :: forall (t1 :: a) (t2 :: a). Sing t1 -> Sing t2 -> Sing (t1 <> t2 :: a) sSconcat :: forall (t :: NonEmpty a). Sing t -> Sing (Sconcat t :: a) default sSconcat :: forall (t :: NonEmpty a). (Sconcat t :: a) ~ SconcatDefault t => Sing t -> Sing (Sconcat t :: a) sSconcat ((sA :: Sing x) :%| (sAs :: Sing xs)) = let sGo :: forall arg1 arg2. Sing arg1 -> Sing arg2 -> Sing (LetGo x xs arg1 arg2) sGo sB (SCons sC sCs) = sB %<> sGo sC sCs sGo sB SNil = sB in sGo sA sAs }}} This typechecks in GHC 8.4/8.6 but fails in HEAD with: {{{ $ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:48:35: error: • Could not deduce (SSemigroup k) arising from a use of ‘%<>’ from the context: SSemigroup a bound by the class declaration for ‘SSemigroup’ at Bug.hs:37:7-16 or from: Sconcat t ~ SconcatDefault t bound by the type signature for: sSconcat :: forall (t :: NonEmpty a). (Sconcat t ~ SconcatDefault t) => Sing t -> Sing (Sconcat t) at Bug.hs:(42,23)-(44,53) or from: t ~ (x ':| xs) bound by a pattern with constructor: :%| :: forall a (x :: a) (xs :: [a]). Sing x -> Sing xs -> Sing (x ':| xs), in an equation for ‘sSconcat’ at Bug.hs:45:13-47 or from: arg2 ~ (x1 : xs1) bound by a pattern with constructor: SCons :: forall a (x :: a) (xs :: [a]). Sing x -> Sing xs -> Sing (x : xs), in an equation for ‘sGo’ at Bug.hs:48:19-30 Possible fix: add (SSemigroup k) to the context of the data constructor ‘SCons’ or the type signature for: sGo :: forall k (arg1 :: k) (arg2 :: [k]). Sing arg1 -> Sing arg2 -> Sing (LetGo x xs arg1 arg2) • In the expression: sB %<> sGo sC sCs In an equation for ‘sGo’: sGo sB (SCons sC sCs) = sB %<> sGo sC sCs In the expression: let sGo :: forall arg1 arg2. Sing arg1 -> Sing arg2 -> Sing (LetGo x xs arg1 arg2) sGo sB (SCons sC sCs) = sB %<> sGo sC sCs sGo sB SNil = sB in sGo sA sAs | 48 | sGo sB (SCons sC sCs) = sB %<> sGo sC sCs | ^^^^^^^^^^^^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15472#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15472: GHC HEAD type inference regression post-"Remove decideKindGeneralisationPlan" -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: highest | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: invalid | 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 monoidal): Thanks. I have simplified the code. {{{#!hs {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind (Type) data Proxy b type family LetGo :: k foo :: Proxy (LetGo :: Type) foo = undefined sSconcat :: forall x. x sSconcat = undefined where sGo :: x -> Proxy LetGo sGo _ = foo }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15472#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15472: GHC HEAD type inference regression post-"Remove decideKindGeneralisationPlan" -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: highest | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: invalid | 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 RyanGlScott): Thanks, monoidal. I've attempted to update the 8.8 Migration Guide ([https://ghc.haskell.org/trac/ghc/wiki/Migration/8.8?version=2#Kindgeneraliza... here]) using this code as an example. goldfire, please shout if my explanation of the issue is wrong is misleading. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15472#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15472: GHC HEAD type inference regression post-"Remove decideKindGeneralisationPlan" -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: highest | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: invalid | 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 simonpj): Would it be possible to give a version of Richard's comment:2 for the nice small program in comment:7? In particular, why does ''more'' generalisation lead to a type error? I'm missing that vital point :-). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15472#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15472: GHC HEAD type inference regression post-"Remove decideKindGeneralisationPlan" -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: highest | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: invalid | 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 RyanGlScott): To see why the program in comment:7 is going awry, suppose the `sGo` function were defined at the top level: {{{#!hs sGo :: x -> Proxy LetGo sGo _ = foo }}} This will not kind-check, before or after the offending commit mentioned above. That's because we always kind-generalize for top-level definitions, so the return kind of `LetGo` will be generalized to `k`, which is too polymorphic for the RHS `foo` (which expects the return kind of `LetGo` to be `Type`). Now, if `sGo` is a locally defined function, as in comment:7: {{{#!hs sSconcat :: forall x. x sSconcat = undefined where sGo :: x -> Proxy LetGo sGo _ = foo }}} Before the offending commit, then the return kind of `LetGo` was //not// generalized, causing it to default to `Type`, which makes everything go through. After the offending commit, however, GHC now kind-generalizes local definitions, which means that the return kind of `LetGo` is now generalized to `k` again. In other words, `sGo` fails to kind-check for the same reasons that it would fail to kind-check if it were defined at the top level. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15472#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15472: GHC HEAD type inference regression post-"Remove decideKindGeneralisationPlan" -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: highest | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: invalid | 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 simonpj): comment:10 makes perfect sense. Making a ''type'' signature more polymorphic than before may indeed make the ''term''-level declaration fail, since it isn't as polymorphic as the (new) signature requires. Thanks. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15472#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC