Ticket #7186: gistfile1.2.hs

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

SingI arity problem example

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 + d) ~  a) => AbsDiff a b d where 
38
39
40
41
42--this doesn't type check
43a ::( AbsDiff 2 1 (d:: Nat ), SingI Nat, (1+d)~ 2)=> Sing d
44a = sing
45
46
47{- Data/TypeLits/GCD.hs:44:5:
48    Could not deduce (SingI Nat d) arising from a use of `sing'
49    from the context (AbsDiff 2 1 d, SingI * Nat, (1 + d) ~ 2)
50      bound by the type signature for
51                 a :: (AbsDiff 2 1 d, SingI * Nat, (1 + d) ~ 2) => Sing Nat d
52      at Data/TypeLits/GCD.hs:43:5-59
53    Possible fix: add an instance declaration for (SingI Nat d)
54    In the expression: sing
55    In an equation for `a': a = sing
56Failed, modules loaded: none. -}