Ticket #7186: gistfile1.hs

File gistfile1.hs, 1.7 KB (added by carter, 20 months ago)

concrete inequality problem (1<=1)

Line 
1{-# LANGUAGE DataKinds #-}              -- to declare the kinds
2{-# LANGUAGE KindSignatures #-}         -- (used all over)
3{-# LANGUAGE TypeFamilies #-}           -- for declaring operators + sing family
4{-# LANGUAGE TypeOperators #-}          -- for declaring operator
5{-# LANGUAGE EmptyDataDecls #-}         -- for declaring the kinds
6{-# LANGUAGE GADTs #-}                  -- for examining type nats
7{-# LANGUAGE PolyKinds #-}              -- for Sing family
8{-# LANGUAGE UndecidableInstances #-}   -- for a bunch of the instances
9{-# LANGUAGE FlexibleInstances #-}      -- for kind parameters
10{-# LANGUAGE FlexibleContexts #-}       -- for kind parameters
11{-# LANGUAGE ScopedTypeVariables #-}    -- for kind parameters\
12{-# LANGUAGE MultiParamTypeClasses #-}  -- for <=, singRep, SingE
13{-# LANGUAGE FunctionalDependencies #-} -- for SingRep and SingE
14
15
16
17
18{-# OPTIONS_GHC -XNoImplicitPrelude #-}
19
20
21   
22
23
24module Data.TypeLits.GCD where
25
26import GHC.TypeLits
27--import GHC.Num(Integer, (-))
28
29
30--class EqNat (a:: Nat) (b :: Nat) where
31
32--instance (SingI a, SingI b, a <= b, b<= a) =>  EqNat a b  where
33
34
35class AbsDiff (a::Nat) (b::Nat)  (d::Nat) | a b -> d where 
36
37instance (SingI  a,SingI  b, SingI  d,(b::Nat) <= (a::Nat), (b + d) ~  a) => AbsDiff a b d where 
38
39
40
41
42--this doesn't type check
43a ::( AbsDiff (2::Nat) (1::Nat) (d:: Nat ), SingI d)=> Sing d
44a = sing
45
46
47{-#
48*Data.TypeLits.GCD> :t a
49
50<interactive>:1:1:
51    Could not deduce (1 <= 2) arising from a use of `a'
52    from the context (SingI Nat d, (1 + d) ~ 2)
53      bound by the inferred type of
54               it :: (SingI Nat d, (1 + d) ~ 2) => Sing Nat d
55      at Top level
56    Possible fix: add an instance declaration for (1 <= 2)
57    In the expression: a
58*Data.TypeLits.GCD>
59
60#-}