T15385.hs 382 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wincomplete-patterns #-}
module T15385 where

import Data.Type.Equality

data T a where
  TInt  :: T Int
  TBool :: T Bool

f1, f2 :: a :~: Int -> T a -> ()
f1 eq t
  | Refl <- eq
  = case t of
      TInt -> ()
f2 eq t
  = if |  Refl <- eq
       -> case t of
            TInt -> ()