ghc
ghc copied to clipboard
Kind synonym hangs
This code hangs. :(
{-# LANGUAGE DeriveDataTypeable, TypeFamilies, TemplateHaskell, DataKinds,
PolyKinds, GADTs, RankNTypes, MultiParamTypeClasses,
FlexibleInstances, UndecidableInstances, UnicodeSyntax,
FunctionalDependencies, StandaloneDeriving,
TypeOperators, ScopedTypeVariables, NoMonomorphismRestriction,
MonadComprehensions, DeriveGeneric, FlexibleContexts,
GeneralizedNewtypeDeriving, ConstraintKinds,
LambdaCase, ViewPatterns, -- AllowAmbiguousTypes,
DefaultSignatures, RecursiveDo, -- ImpredicativeTypes,
ImplicitParams, MagicHash, UnboxedTuples, RoleAnnotations,
ExtendedDefaultRules, PatternSynonyms, EmptyCase,
BangPatterns, InstanceSigs, DeriveFunctor, Arrows
, NamedWildCards, PartialTypeSignatures
, TypeInType, TypeApplications, TypeFamilyDependencies
-- , OverloadedLists
#-}
module Scratch where
import Data.Singletons
import GHC.Types
import Data.Proxy
-- type NewKindOf (a :: k) = ('Proxy :: Proxy k)
type NewKindOf (a :: k) = k
type a ~> b = TyFun a b -> *
infixr 0 ~>
type family Lam_ayN9 f_ayN5
g_ayN6
a_1627523689_ayN7
t_ayNb where
Lam_ayN9 f_ayN5 g_ayN6 a_1627523689_ayN7 x_ayNa = Apply f_ayN5 (Apply g_ayN6 x_ayNa)
type LamSym4 t_ayNc t_ayNd t_ayNe t_ayNf =
Lam_ayN9 t_ayNc t_ayNd t_ayNe t_ayNf
data LamSym3 l_ayNq l_ayNr l_ayNs l_ayNp
= forall arg_ayNt. ('Proxy :: Proxy (NewKindOf (Apply (LamSym3 l_ayNq l_ayNr l_ayNs) arg_ayNt))) ~ ('Proxy :: Proxy (NewKindOf (LamSym4 l_ayNq l_ayNr l_ayNs arg_ayNt))) =>
LamSym3KindInference
type instance Apply (LamSym3 l_ayNq l_ayNr l_ayNs) l_ayNp = LamSym4 l_ayNq l_ayNr l_ayNs l_ayNp
data LamSym2 l_ayNm l_ayNn l_ayNl
= forall arg_ayNo. NewKindOf (Apply (LamSym2 l_ayNm l_ayNn) arg_ayNo) ~ NewKindOf (LamSym3 l_ayNm l_ayNn arg_ayNo) =>
LamSym2KindInference
type instance Apply (LamSym2 l_ayNm l_ayNn) l_ayNl = LamSym3 l_ayNm l_ayNn l_ayNl
data LamSym1 l_ayNj l_ayNi
= forall arg_ayNk. NewKindOf (Apply (LamSym1 l_ayNj) arg_ayNk) ~ NewKindOf (LamSym2 l_ayNj arg_ayNk) =>
LamSym1KindInference
type instance Apply (LamSym1 l_ayNj) l_ayNi = LamSym2 l_ayNj l_ayNi
data LamSym0 l_ayNg
= forall arg_ayNh. NewKindOf (Apply LamSym0 arg_ayNh) ~ NewKindOf (LamSym1 arg_ayNh) =>
LamSym0KindInference
type instance Apply LamSym0 l_ayNg = LamSym1 l_ayNg
type (:.$$$$) (t_ayMO :: b1627523667 ~> c1627523668)
(t_ayMP :: a1627523669 ~> b1627523667)
(t_ayMQ :: a1627523669) =
(:.) t_ayMO t_ayMP t_ayMQ
data (:.$$$) (l_ayMX :: b1627523667 ~> c1627523668)
(l_ayMY :: a1627523669 ~> b1627523667)
(l_ayMW :: TyFun a1627523669 c1627523668)
= forall arg_ayMZ. NewKindOf (Apply ((:.$$$) l_ayMX l_ayMY) arg_ayMZ) ~ NewKindOf ((:.$$$$) l_ayMX l_ayMY arg_ayMZ) =>
(:.$$$###)
type instance Apply ((:.$$$) l_ayMX l_ayMY) l_ayMW = (:.$$$$) l_ayMX l_ayMY l_ayMW
data (:.$$) (l_ayMU :: b1627523667 ~> c1627523668)
(l_ayMT :: TyFun (a1627523669 ~> b1627523667) (a1627523669 ~> c1627523668))
= forall arg_ayMV. NewKindOf (Apply ((:.$$) l_ayMU) arg_ayMV) ~ NewKindOf ((:.$$$) l_ayMU arg_ayMV) =>
(:.$$###)
type instance Apply ((:.$$) l_ayMU) l_ayMT = (:.$$$) l_ayMU l_ayMT
data (:.$) (l_ayMR :: TyFun (b1627523667 ~> c1627523668) ((a1627523669 ~> b1627523667) ~> (a1627523669 ~> c1627523668)))
= forall arg_ayMS. NewKindOf (Apply (:.$) arg_ayMS) ~ NewKindOf ((:.$$) arg_ayMS) =>
(:.$###)
type instance Apply (:.$) l_ayMR = (:.$$) l_ayMR
type family (:.) (a_ayN0 :: b_ayMH ~> c_ayMI)
(a_ayN1 :: a_ayMJ ~> b_ayMH)
(a_ayN2 :: a_ayMJ) :: c_ayMI where
(:.) f_ayN5 g_ayN6 a_1627523689_ayN7 = Apply (Apply (Apply (Apply LamSym0 f_ayN5) g_ayN6) a_1627523689_ayN7) a_1627523689_ayN7
infixr 9 :.
infixr 9 %:.
(%:.) ::
forall (t_ayNu :: b_ayMH ~> c_ayMI)
(t_ayNv :: a_ayMJ ~> b_ayMH)
(t_ayNw :: a_ayMJ).
Sing t_ayNu
-> Sing t_ayNv
-> Sing t_ayNw
-> Sing (Apply (Apply (Apply (:.$) t_ayNu) t_ayNv) t_ayNw :: c_ayMI)
(%:.) sF sG sA_1627523689
= let
lambda_ayNx ::
forall f_ayN5 g_ayN6 a_1627523689_ayN7.
(t_ayNu ~ f_ayN5, t_ayNv ~ g_ayN6, t_ayNw ~ a_1627523689_ayN7) =>
Sing f_ayN5
-> Sing g_ayN6
-> Sing a_1627523689_ayN7
-> Sing (Apply (Apply (Apply (:.$) t_ayNu) t_ayNv) t_ayNw :: c_ayMI)
lambda_ayNx f_ayNy g_ayNz a_1627523689_ayNA
= applySing
(singFun1
(Proxy ::
Proxy (Apply (Apply (Apply LamSym0 f_ayN5) g_ayN6) a_1627523689_ayN7))
(\ sX
-> let
lambda_ayNB ::
forall x_ayNa.
Sing x_ayNa
-> Sing (Apply (Apply (Apply (Apply LamSym0 f_ayN5) g_ayN6) a_1627523689_ayN7) x_ayNa)
lambda_ayNB x_ayNC = applySing f_ayNy (applySing g_ayNz x_ayNC)
in lambda_ayNB sX))
a_1627523689_ayNA
in lambda_ayNx sF sG sA_1627523689
It has something to do with the use of a kind synonym in ('Proxy :: Proxy (NewKindOf ...)).