[GHC] #15472: GHC HEAD type inference regression post-"Remove decideKindGeneralisationPlan"
GHC
ghc-devs at haskell.org
Fri Aug 3 14:49:59 UTC 2018
#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
More information about the ghc-tickets
mailing list