summaryrefslogtreecommitdiff
path: root/testsuite/tests/typecheck/should_fail/T16512a.hs
blob: 120fb00d97fc60d216876b2d73b30932ef6c229c (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE ViewPatterns           #-}
{-# LANGUAGE UndecidableInstances   #-}

module T16512a where

import Data.Kind
  ( Type )

-- HOAS representation
data AST (a :: Type) :: Type where
  (:$) :: AST ( a -> b ) -> AST a -> AST b
  -- Lam :: ( AST a -> AST b ) -> AST ( a -> b )
  -- PrimOp :: PrimOp op a => AST a
  -- ...

data ASTs (as :: [Type]) :: Type where
  NilASTs :: ASTs '[]
  ConsAST :: AST a -> ASTs as -> ASTs (a ': as)

type family ListVariadic (as :: [Type]) (b :: Type) = (r :: Type) | r -> as b where
  ListVariadic (a ': as) b = a -> ListVariadic as b
  -- ListVariadic '[] ()     = ()
  -- ListVariadic '[] Bool   = Bool
  -- ListVariadic '[] Word   = Word
  -- ListVariadic '[] Int    = Int
  -- ListVariadic '[] Float  = Float
  -- ListVariadic '[] Double = Double
  -- ...

data AnApplication b where
  AnApplication :: AST (ListVariadic as b) -> ASTs as -> AnApplication b

unapply :: AST b -> AnApplication b
unapply (f :$ a)
  = case unapply f of
        AnApplication g as ->
          AnApplication g (a `ConsAST` as)
-- no other cases with this simplified AST