testsuite/tests/tcplugins/TcPlugin_Rewrite.hs


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

{-# OPTIONS_GHC -dcore-lint #-}
{-# OPTIONS_GHC -fplugin RewritePlugin #-}

{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE DataKinds, ScopedTypeVariables, TypeFamilies, TypeOperators #-}

module TcPlugin_Rewrite where

import Data.Kind
  ( Type )

import Data.Type.Equality
  ( type (~) )

import Definitions
  ( Add, Nat(..) )


foo :: forall (proxy :: Nat -> Type) (n :: Nat)
    .  ( Add Zero n ~ n )
    => proxy n -> ()
foo _ = ()

bar :: forall (proxy :: Nat -> Type) (n :: Nat)
    .  proxy n -> ()
bar n = foo n