This is the code from #38, with a typed hole instead of the expression causing the error.
{-# 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 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 [])
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)
$(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 -- ft `unSLambda` fr `unSLambda` fq `unSLambda` fp
}
)))))
OUT.hs:231:100: Warning:ghc: panic! (the 'impossible' happened)
(GHC version 7.11.20150702 for x86_64-unknown-linux):
No skolem info: jz_a4t8
This is the code from #38, with a typed hole instead of the expression causing the error.