Commit 2f946237 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Test Trac #3484

parent 99e6b7b0
{-# 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
......@@ -162,3 +162,4 @@ test('T4494', normal, compile, [''])
test('DataFamDeriv', normal, compile, [''])
test('T1769', if_compiler_lt('ghc', '7.1', expect_fail), compile, [''])
test('T4497', normal, compile, [''])
test('T3484', normal, compile, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment