Kind unification error (or unhelpful error message ?)

[RafaelBocquet]

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 ?

[goldfirere]

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?

[RafaelBocquet]

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.

[goldfirere]

Not this week -- sorry. Doing a frantic run to put together a POPL paper.
Next week should be OK, though.

[goldfirere]

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.