ghc
ghc copied to clipboard
goldfirere
Kind unification error (or unhelpful error message ?)
It seems in this case that ghc is able to check t : k1 and t : k2, but fails to unify k1 with k2 (t=AH t t6 t2 t7 t4 t7, k1=T t (H t6 t2 t6) and k2=T t (H jv jz jv)).
The example is quite long, but I don't know how to make it shorter...
The error is ~5 lines from the end (Actual type = type of SCons _ _ _ _)
{-# LANGUAGE GADTs, RankNTypes, DataKinds, PolyKinds, TypeFamilies, TypeOperators, ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, FlexibleContexts #-}
{-# LANGUAGE TemplateHaskell, EmptyCase, PartialTypeSignatures, NoMonomorphismRestriction, ImpredicativeTypes #-}
{-# OPTIONS_GHC -fno-max-relevant-binds #-}
{-# OPTIONS_GHC -fwarn-unticked-promoted-constructors #-}
module OUT where
import Prelude ()
import qualified Prelude as P
import qualified Language.Haskell.TH as TH
data family Sing (k :: *) :: k -> *
type Sing' (x :: k) = Sing k x
type family FromSing (y :: Sing k x) where
FromSing (y :: Sing k x) = x
type family ToSing (x :: k) :: Sing k x
class SingKind (k :: *) where
fromSing :: Sing k x -> k
toSing :: k -> SomeSing k
data SomeSing (k :: *) where SomeSing :: forall (k :: *) (x :: k). Sing k x -> SomeSing k
$(do P.return [])
data instance Sing * x where
SStar :: forall (x :: *). Sing * x
$(do P.return [])
type instance ToSing (x :: *) = 'SStar
$(do P.return [])
data TyFun' (a :: *) (b :: *) :: *
type TyFun (a :: *) (b :: *) = TyFun' a b -> *
type family (a :: TyFun k1 k2) @@ (b :: k1) :: k2
data TyPi' (a :: *) (b :: TyFun a *) :: *
type TyPi (a :: *) (b :: TyFun a *) = TyPi' a b -> *
type family (a :: TyPi k1 k2) @@@ (b :: k1) :: k2 @@ b
data instance Sing (TyPi k1 k2) x where
SLambda :: (forall (t :: k1). Sing k1 t -> Sing (k2 @@ t) (f @@@ t)) -> Sing (TyPi k1 k2) f
unSLambda :: Sing (TyPi k1 k2) f -> (forall t. Sing k1 t -> Sing (k2 @@ t) (f @@@ t))
unSLambda (SLambda x) = x
$(do TH.reportWarning "A"; P.return [])
$(P.return [])
data Nat :: * where
O :: forall. Nat
S :: forall. Nat -> Nat
$(P.return [])
data T (e :: *) (f :: Nat) :: * where
Nil :: forall (a :: *). Sing * a -> T a 'O
Cons :: forall (b :: *) (c :: b) (d :: Nat). Sing * b -> Sing b c -> Sing Nat d -> T b d -> T b ('S d)
$(P.return [])
data instance Sing (T m n) l where
SNil :: forall (g :: *). Sing * g -> Sing' ('Nil (ToSing g))
SCons ::
forall (h :: *) (i :: h) (j :: Nat) (k :: T h j). Sing * h -> Sing h i -> Sing Nat j -> Sing (T h j) k -> Sing'
('Cons (ToSing h) (ToSing i) (ToSing j) k)
$(P.return [])
data instance Sing Nat p where
SO :: forall. Sing' 'O
SS :: forall (o :: Nat). Sing Nat o -> Sing' ('S o)
$(P.return [])
data G (s :: Nat) (r :: Nat) (q :: TyFun' Nat *)
$(P.return [])
type instance (@@) (G v u) t = Nat
$(P.return [])
data F (y :: Nat) (x :: Nat) (w :: TyPi' Nat (G y x))
$(P.return [])
data A (aa :: Nat) (z :: TyFun' Nat *)
$(P.return [])
type instance (@@) (A ac) ab = Nat
$(P.return [])
data I (ae :: Nat) (ad :: TyPi' Nat (A ae))
$(P.return [])
data B (af :: TyFun' Nat *)
$(P.return [])
type instance (@@) B ag = TyPi Nat (A ag)
$(P.return [])
data J (ah :: TyPi' Nat B)
$(P.return [])
type family C :: TyPi Nat B where
C = J
$(P.return [])
data AB (ba :: *) (az :: Nat) (ay :: Nat) (ax :: T ba az) (aw :: T ba ay) (av :: ba) (au :: Nat) (at :: TyFun' (T ba au) *)
$(P.return [])
type instance (@@) (AB bi bh bg bf be bd bc) bb = T bi ('S (C @@@ bc @@@ bg))
$(P.return [])
data AD (bq :: *) (bp :: Nat) (bo :: Nat) (bn :: T bq bp) (bm :: T bq bo) (bl :: bq) (bk :: Nat) (bj :: TyPi' (T bq bk) (AB bq bp bo bn bm bl bk))
$(P.return [])
data AC (bx :: *) (bw :: Nat) (bv :: Nat) (bu :: T bx bw) (bt :: T bx bv) (bs :: bx) (br :: TyFun' Nat *)
$(P.return [])
type instance (@@) (AC ce cd cc cb ca bz) by = TyPi (T ce by) (AB ce cd cc cb ca bz by)
$(P.return [])
data AE (cl :: *) (ck :: Nat) (cj :: Nat) (ci :: T cl ck) (ch :: T cl cj) (cg :: cl) (cf :: TyPi' Nat (AC cl ck cj ci ch cg))
$(P.return [])
data AG (cr :: *) (cq :: Nat) (cp :: Nat) (co :: T cr cq) (cn :: T cr cp) (cm :: TyFun' cr *)
$(P.return [])
type instance (@@) (AG cx cw cv cu ct) cs = TyPi Nat (AC cx cw cv cu ct cs)
$(P.return [])
data AF (dd :: *) (dc :: Nat) (db :: Nat) (da :: T dd dc) (cz :: T dd db) (cy :: TyPi' dd (AG dd dc db da cz))
$(P.return [])
data P (di :: *) (dh :: Nat) (dg :: Nat) (df :: T di dh) (de :: TyFun' (T di dg) *)
$(P.return [])
type instance (@@) (P dn dm dl dk) dj = T dn (C @@@ dm @@@ dl)
$(P.return [])
data AI (dt :: *) (ds :: Nat) (dr :: Nat) (dq :: T dt ds) (dp :: TyPi' (T dt dr) (P dt ds dr dq))
$(P.return [])
data Q (dx :: *) (dw :: Nat) (dv :: Nat) (du :: TyFun' (T dx dw) *)
$(P.return [])
type instance (@@) (Q eb ea dz) dy = TyPi (T eb dz) (P eb ea dz dy)
$(P.return [])
data AJ (ef :: *) (ee :: Nat) (ed :: Nat) (ec :: TyPi' (T ef ee) (Q ef ee ed))
$(P.return [])
data R (ei :: *) (eh :: Nat) (eg :: TyFun' Nat *)
$(P.return [])
type instance (@@) (R el ek) ej = TyPi (T el ek) (Q el ek ej)
$(P.return [])
data AK (eo :: *) (en :: Nat) (em :: TyPi' Nat (R eo en))
$(P.return [])
data U (eq :: *) (ep :: TyFun' Nat *)
$(P.return [])
type instance (@@) (U es) er = TyPi Nat (R es er)
$(P.return [])
data AL (eu :: *) (et :: TyPi' Nat (U eu))
$(P.return [])
data V (ev :: TyFun' * *)
$(P.return [])
type instance (@@) V ew = TyPi Nat (U ew)
$(P.return [])
data AM (ex :: TyPi' * V)
$(P.return [])
type family W :: TyPi * V where
W = AM
$(P.return [])
type instance (@@@) AM gc = AL gc
$(P.return [])
type instance (@@@) (AL ge) gd = AK ge gd
$(P.return [])
type instance (@@@) (AK gh gg) gf = AJ gh gg gf
$(P.return [])
type instance (@@@) (AJ gl gk gj) gi = AI gl gk gj gi
$(P.return [])
data AA (gr :: *) (gq :: Nat) (gp :: Nat) (go :: T gr gq) (gn :: T gr gp) (gm :: TyFun' Nat *)
$(P.return [])
data X (gy :: *) (gx :: Nat) (gw :: Nat) (gv :: T gy gx) (gu :: T gy gw) (gt :: Nat) (gs :: TyFun' (T gy gt) *)
$(P.return [])
type instance (@@) (X hf he hd hc hb ha) gz = *
$(P.return [])
type instance (@@) (AA hl hk hj hi hh) hg = TyPi (T hl hg) (X hl hk hj hi hh hg)
$(P.return [])
data Z (hr :: *) (hq :: Nat) (hp :: Nat) (ho :: T hr hq) (hn :: T hr hp) (hm :: TyPi' Nat (AA hr hq hp ho hn))
$(P.return [])
type instance (@@@) (AF hx hw hv hu ht) hs = AE hx hw hv hu ht hs
$(P.return [])
data Y (ie :: *) (id :: Nat) (ic :: Nat) (ib :: T ie id) (ia :: T ie ic) (hz :: Nat) (hy :: TyPi' (T ie hz) (X ie id ic ib ia hz))
$(P.return [])
type instance (@@@) (Z il ik ij ii ih) ig = Y il ik ij ii ih ig
$(P.return [])
data E (ky :: Nat) (kx :: Nat) (kw :: TyFun' Nat *)
$(P.return [])
type instance (@@) (E lb la) kz = *
$(P.return [])
data D (le :: Nat) (ld :: Nat) (lc :: TyPi' Nat (E le ld))
$(P.return [])
type instance (@@@) (D lh lg) lf = Nat
$(P.return [])
type instance (@@@) (F lk lj) li = 'S (C @@@ li @@@ lj)
$(P.return [])
type family H (ls :: Nat) (lr :: Nat) (lq :: Nat) :: Nat where
H lm ll 'O = ll
H lp lo ('S ln) = F lp lo @@@ ln
$(P.return [])
type instance (@@@) (AE jt js jr jq jp jo) jn = AD jt js jr jq jp jo jn
$(P.return [])
type instance (@@@) (AD kb ka jz jy jx jw jv) ju = 'Cons (ToSing kb) (ToSing jw) (ToSing (C @@@ jv @@@ jz)) (W @@@ kb
@@@ jv @@@ jz @@@ ju @@@ jx)
$(P.return [])
type family AH (jh :: *) (jg :: Nat) (jf :: Nat) (je :: T jh jg) (jd :: T jh jf) (jc :: T jh jg) :: T jh (H jg jf jg) where
AH is 'O iq ip io ('Nil im) = io
AH jb ('S ja) iz iy ix ('Cons it iu iv iw) = AD jb ('S ja) iz iy ix (FromSing iu) (FromSing iv) @@@ iw
$(P.return [])
data L (kj :: TyFun' * *)
$(P.return [])
data N (kl :: *) (kk :: TyFun' Nat *)
$(P.return [])
type instance (@@) (N kn) km = *
$(P.return [])
type instance (@@) L ko = TyPi Nat (N ko)
$(P.return [])
data K (kp :: TyPi' * L)
$(P.return [])
data M (kr :: *) (kq :: TyPi' Nat (N kr))
$(P.return [])
type instance (@@@) K ks = M ks
$(P.return [])
type instance (@@@) (M ku) kt = T ku kt
$(P.return [])
type instance (@@@) J kv = I kv
$(P.return [])
$(P.return [])
type instance (@@@) (I lu) lt = H lu lt lu
$(P.return [])
type instance (@@@) (AI jm jl jk jj) ji = AH jm jl jk jj ji jj
$(P.return [])
type instance (@@@) (Y ki kh kg kf ke kd) kc = T ki (C @@@ kd @@@ kg)
$(P.return [])
add :: Sing' C
add = let { ai = let { aj :: Sing' J; aj = SLambda (\(al :: Sing Nat ak) -> let { am :: Sing' (I ak); am = SLambda
(\(ao :: Sing Nat an) -> case al of { SO -> ao; SS ap -> let { aq :: Sing' (F ak an); aq = SLambda (\(as :: Sing Nat
ar) -> SS (ai `unSLambda` as `unSLambda` ao))} in aq `unSLambda` ap })} in am)} in aj; } in ai
$(P.return [])
append :: Sing' W
append = SLambda (\(fb :: Sing * fa) ->
SLambda (\(fe :: Sing Nat fd) ->
SLambda (\(fh :: Sing Nat fg) ->
SLambda (\(fk :: Sing (T fa fd) fj) ->
SLambda (\(fn :: Sing (T fa fg) fm) -> case fk of
{ SNil fo -> fn
; SCons fs fr fq fp ->
let { ft :: Sing' (AF fa fd fg fj fm)
; ft = SLambda (\(fv :: Sing fa fu) ->
SLambda (\(fy :: Sing Nat fx) ->
SLambda (\(gb :: Sing (T fa fx) ga) ->
SCons fb fv
(add `unSLambda` fy `unSLambda` fh)
(append `unSLambda` fb `unSLambda` fy `unSLambda` fh `unSLambda` gb `unSLambda` fn)
))
)
} in P.undefined
}
)))))
With normalised types, we get a "Can't unify t with t" error message :
OUT.hs:233:133:
Could not deduce (H t6 t2 t6 ~ H jv jz jv)
from the context (t1 ~ 'S j,
t3 ~ 'Cons (ToSing t) (ToSing i) (ToSing j) k)
bound by a pattern with constructor
SCons :: forall h (j :: Nat) (i :: h) (k :: T h j).
Sing * h
-> Sing h i
-> Sing Nat j
-> Sing (T h j) k
-> Sing' ('Cons (ToSing h) (ToSing i) (ToSing j) k),
in a case alternative
at OUT.hs:227:78-94
NB: ‘H’ is a type function, and may not be injective
When matching types
AH t t6 t2 t7 t4 t7 :: T t (H t6 t2 t6)
AH t t6 t2 t7 t4 t7 :: T t (H jv jz jv)
Expected type: Sing
(AB t ('S j) t2 ('Cons 'SStar (ToSing i) (ToSing j) k) t4 t5 t6
@@ t7)
(AD t ('S j) t2 ('Cons 'SStar (ToSing i) (ToSing j) k) t4 t5 t6
@@@ t7)
Actual type: Sing
(T t ('S (H t6 t2 t6)))
('Cons
'SStar (ToSing t5) (ToSing (H t6 t2 t6)) (AH t t6 t2 t7 t4 t7))
With "normaliseType fam_envs Representational":
Expected type: OUT.R:SingTl
t
('S (H t6 t2 t6))
('Cons 'SStar (ToSing t5) (ToSing (H t6 t2 t6)) (AH
t t6 t2 t7 t4 t7))
Actual type: OUT.R:SingTl
t
('S (H t6 t2 t6))
('Cons
'SStar (ToSing t5) (ToSing (H t6 t2 t6)) (AH t t6 t2 t7 t4 t7))
Relevant bindings include
gb :: Sing (T t t6) t7 (bound at OUT.hs:232:133)
fy :: Sing Nat t6 (bound at OUT.hs:231:122)
fw :: Sing' (AE t t1 t2 t3 t4 t5) (bound at OUT.hs:231:106)
fv :: Sing t t5 (bound at OUT.hs:229:100)
ft :: Sing' (AF t t1 t2 t3 t4) (bound at OUT.hs:229:84)
fp :: Sing (T t j) k (bound at OUT.hs:227:93)
fr :: Sing t i (bound at OUT.hs:227:87)
fs :: Sing * t (bound at OUT.hs:227:84)
fn :: Sing (T t t2) t4 (bound at OUT.hs:225:65)
fk :: Sing (T t t1) t3 (bound at OUT.hs:224:54)
fh :: Sing Nat t2 (bound at OUT.hs:223:43)
fb :: Sing * t (bound at OUT.hs:221:21)
In the expression:
SCons
fb
fv
(add `unSLambda` fy `unSLambda` fh)
(append `unSLambda` fb `unSLambda` fy `unSLambda` fh `unSLambda` gb
`unSLambda` fn)
In the first argument of ‘SLambda’, namely
‘(\ (gb :: Sing (T fa fx) ga)
-> SCons
fb
fv
(add `unSLambda` fy `unSLambda` fh)
(append `unSLambda` fb `unSLambda` fy `unSLambda` fh `unSLambda` gb
`unSLambda` fn))’
Using the flag -fprint-explicit-kinds, we get :
When matching types
AH t t6 t2 t7 t4 t7 :: T t (H t6 t2 t6)
(AH t t6 t2 t7 t4 t7 |> {- coercion -} :: T t (H jv jz jv)
Shouldn't the coercion contain the needed proof ?
I get this:
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 7.11.20150225 for x86_64-apple-darwin):
ASSERT failed!
file compiler/types/Coercion.hs line 1024
Sub (TFCo:R:@@TYPENatBag[0] <jv_a4tA>_N) representational
What commit are you working from?
Sorry, I had disabled this assertion as it allowed me to compile/run some programs, and I thought I had checked it was not caused by this before submitting the issue.
I can move the error from
type instance (@@@) (AD kb ka jz jy jx jw jv) ju = 'Cons (ToSing kb) (ToSing jw) (ToSing (C @@@ jv @@@ jz)) (W @@@ kb
@@@ jv @@@ jz @@@ ju @@@ jx)
to the code in append by reducing it to
type instance (@@@) (AD kb ka jz jy jx jw jv) ju = 'Cons (ToSing kb) (ToSing jw) (ToSing (H jv jz jv)) (AH kb jv jz ju jx ju)
and moving AD after H and AH.
ghc: panic! (the 'impossible' happened)
(GHC version 7.11.20150702 for x86_64-unknown-linux):
ASSERT failed!
file compiler/types/Coercion.hs line 1024
Sym cobox_a4TI representational
The error is the same as in #32. As it can be avoided by reducing type families, it may be related to them.
Can you look into this ?
#39 is independent, I updated its code so as not to trigger this assertion.
Not this week -- sorry. Doing a frantic run to put together a POPL paper. Next week should be OK, though.
I have a vague idea of what's going on.
From your original post:
When matching types
AH t t6 t2 t7 t4 t7 :: T t (H t6 t2 t6)
(AH t t6 t2 t7 t4 t7 |> {- coercion -} :: T t (H jv jz jv)
Shouldn't the coercion contain the needed proof ?
No. The reason is that the coercion there is representational, and GHC is looking for a nominal proof. If your code depends on using that coercion to type-check, GHC is doing the right thing here.
One of my tasks over the next month is to smooth out roles in kind coercions, by having all kind coercions be at nominal role. This is much simpler than the current story. But it prevents promotion of Core code that wraps/unwraps newtypes. This is OK, because promotion of Core code is not yet implemented -- we only promote Haskell code, which remains fine. Getting rid of roles in kinds does make implementing Pi harder, but Simon PJ's (always sage) advice is to do the simple thing today and let tomorrow worry about the complex thing. So I'll simplify (it's not actually much code to change) and then worry about this issue later. One effect of this will be that this ticket should get resolved.