blob: bba4c1df185adcfea005cacbcc718ab34007dbbc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Main where
data Proxy (a :: k) = Proxy
data Con k (a :: k) = Con (Proxy a)
tyApp :: Con k a -> Proxy a
tyApp (Con @kx @ax (x :: Proxy ax)) = x :: Proxy (ax :: kx)
main = return ()
|
