search

goldfirere / ghc

Mirror of ghc repository. DO NOT SUBMIT PULL REQUESTS HERE
http://www.haskell.org/ghc/
Other
25 stars 1 forks source link

Kind synonym hangs #68

Open goldfirere opened 8 years ago

goldfirere commented 8 years ago

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
goldfirere commented 8 years ago

It has something to do with the use of a kind synonym in ('Proxy :: Proxy (NewKindOf ...)).