diff options
Diffstat (limited to 'testsuite/tests/ghc-regress/indexed-types/should_compile/T3484.hs')
-rw-r--r-- | testsuite/tests/ghc-regress/indexed-types/should_compile/T3484.hs | 42 |
1 files changed, 0 insertions, 42 deletions
diff --git a/testsuite/tests/ghc-regress/indexed-types/should_compile/T3484.hs b/testsuite/tests/ghc-regress/indexed-types/should_compile/T3484.hs deleted file mode 100644 index 4d1570915e..0000000000 --- a/testsuite/tests/ghc-regress/indexed-types/should_compile/T3484.hs +++ /dev/null @@ -1,42 +0,0 @@ -{-# LANGUAGE GADTs, RankNTypes, TypeFamilies, FlexibleContexts, ScopedTypeVariables #-} -{-# OPTIONS_GHC -Wall #-} -module Absurd where - -data Z = Z -newtype S n = S n -class Nat n where - caseNat :: (n ~ Z => r) -> (forall p. (n ~ S p, Nat p) => p -> r) -> n -> r -instance Nat Z where - caseNat = error "urk1" -instance Nat n => Nat (S n) where - caseNat = error "urk2" - --- empty type -newtype Naught = Naught (forall a. a) --- types are equal! -data TEq a b where - TEq :: (a ~ b) => TEq a b - -type family NatEqProves m n -type instance NatEqProves (S m) (S n) = TEq m n - -noConf :: (Nat m, Nat n) => m -> TEq m n -> NatEqProves m n -noConf = undefined -predEq :: TEq (S a) (S b) -> TEq a b -predEq = undefined - -data IsEq a b = Yes (TEq a b) | No (TEq a b -> Naught) - -natEqDec :: forall m n. (Nat m, Nat n) => m -> n -> IsEq m n -natEqDec m n = caseNat undefined mIsS m where - mIsS :: forall pm. (m ~ S pm, Nat pm) => pm -> IsEq m n - mIsS pm = caseNat undefined nIsS n where - nIsS :: forall pn. (n ~ S pn, Nat pn) => pn -> IsEq m n - nIsS pn = case natEqDec pm pn of - Yes TEq -> Yes TEq - No contr -> No (contr . noConf m) --- No contr -> No (contr . predEq) - --- strange things: --- (1) commenting out the "Yes" case or changing it to "undefined" makes compilation succeed --- (2) replacing the "No" line with with the commented out "No" line makes compilation succeed
\ No newline at end of file |