blob: d19bd2355c1141e1e5aa1014a19afaf708ec2286 (
plain)
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
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
-- This program is an example of a use of UndecidableInstances and
-- QuantifiedConstraints which circumvents the usual compile-time solver
-- termination check and instead produces a program which loops at runtime.
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeOperators #-}
import System.IO
import Data.Void
import Data.Typeable
import Data.Type.Equality
class (forall k. k a => k b) => Equ a b
instance Equ a a
data Z' a where
Z' :: Z' Void
data Z where
Z :: forall a. Equ Void a => Z' a -> Z
checkZ :: Z -> Bool
checkZ (Z (Z' :: Z' a)) = case eqT of
Nothing -> False
Just (Refl :: a :~: Void) -> True
main :: IO ()
main = do
hPutStrLn stderr "before..."
hPutStrLn stderr $ show $ checkZ $ Z Z'
hPutStrLn stderr "after!"
|
