T8031.hs 368 Bytes
Newer Older
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
1
{-# LANGUAGE TemplateHaskell, RankNTypes, TypeOperators, TypeInType,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
2 3 4 5 6
             GADTs #-}

module T8031 where

import Data.Proxy
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
7
import Data.Kind
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
8 9 10

data SList :: [k] -> * where
  SCons :: Proxy h -> Proxy t -> SList (h ': t)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
11

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
12 13 14 15
$( [d| foo :: forall (a :: k). Proxy a
           -> forall (b :: [k]). Proxy b
           -> SList (a ': b)
       foo a b = SCons a b |] )