blob: 72f85dddd6e222a7f725b160e7f530b42464c091 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wall #-}
module T17270 where
import Data.Type.Equality
f :: a :~: Int -> b :~: Bool -> a :~: b -> void
f Refl Refl x = case x of {}
$([d| g :: a :~: Int -> b :~: Bool -> a :~: b -> void
g Refl Refl x = case x of {}
|])
|
