Type inference
--Copyright (C) 2017 Zaoqi
--This program is free software: you can redistribute it and/or modify
--it under the terms of the GNU Affero General Public License as published
--by the Free Software Foundation, either version 3 of the License, or
--(at your option) any later version.
--This program is distributed in the hope that it will be useful,
--but WITHOUT ANY WARRANTY; without even the implied warranty of
--MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
--GNU Affero General Public License for more details.
--You should have received a copy of the GNU Affero General Public License
--along with this program. If not, see <http://www.gnu.org/licenses/>.
{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}
import Control.Exception
data Nat = Z | S Nat deriving (Eq, Ord)
instance Enum Nat where
succ = S
pred (S x) = x
pred _ = throw Underflow
toEnum 0 = Z
toEnum x | x < 0 = throw Underflow
| otherwise = S . toEnum $ pred x
fromEnum Z = 0
fromEnum (S x) = succ $ fromEnum x
enumFrom x = x : enumFrom (S x)
instance Num Nat where
Z + x = x
(S x) + y = S $ x + y
Z * _ = Z
(S x) * y = y + (x * y)
abs = id
signum Z = Z
signum _ = S Z
fromInteger 0 = Z
fromInteger x | x < 0 = throw Underflow
| otherwise = S . fromInteger $ pred x
x - Z = x
(S x) - (S y) = x - y
_ - _ = throw Underflow
negate Z = Z
negate _ = throw Underflow
instance Real Nat where
toRational = toRational . toInteger
instance Integral Nat where
quot x y = fromInteger $ quot (toInteger x) (toInteger y)
rem x y = fromInteger $ rem (toInteger x) (toInteger y)
div x y = fromInteger $ div (toInteger x) (toInteger y)
mod x y = fromInteger $ mod (toInteger x) (toInteger y)
quotRem x y = let (x, y) = quotRem (toInteger x) (toInteger y) in (fromInteger x, fromInteger y)
divMod x y = let (x, y) = divMod (toInteger x) (toInteger y) in (fromInteger x, fromInteger y)
toInteger Z = 0
toInteger (S x) = succ $ toInteger x
data Vec :: Nat -> * -> * where
Nil :: Vec Z a
Cons :: a -> Vec x a -> Vec (S x) a
data ReadableVec :: * -> * where
ReadableVec :: Vec x a -> ReadableVec a
instance Read a => Read (ReadableVec a) where
readsPrec x s = map (\(xs, r) -> (l2rv xs, r)) (readsPrec x s)
where
l2rv [] = ReadableVec Nil
l2rv (x : xs) = case l2rv xs of
ReadableVec rs -> ReadableVec (Cons x rs)
instance Show a => Show (Vec x a) where
showsPrec p xs = showsPrec p (ReadableVec xs)
instance Show a => Show (ReadableVec a) where
showsPrec p xs = showsPrec p (rv2l xs)
where
rv2l :: ReadableVec x -> [x]
rv2l (ReadableVec Nil) = []
rv2l (ReadableVec (Cons x xs)) = x : rv2l (ReadableVec xs)GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Prelude> :load Vec.hs
[1 of 1] Compiling Main ( Vec.hs, interpreted )
Ok, modules loaded: Main.--Copyright (C) 2017 Zaoqi
--This program is free software: you can redistribute it and/or modify
--it under the terms of the GNU Affero General Public License as published
--by the Free Software Foundation, either version 3 of the License, or
--(at your option) any later version.
--This program is distributed in the hope that it will be useful,
--but WITHOUT ANY WARRANTY; without even the implied warranty of
--MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
--GNU Affero General Public License for more details.
--You should have received a copy of the GNU Affero General Public License
--along with this program. If not, see <http://www.gnu.org/licenses/>.
{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}
import Control.Exception
data Nat = Z | S Nat deriving (Eq, Ord)
instance Enum Nat where
succ = S
pred (S x) = x
pred _ = throw Underflow
toEnum 0 = Z
toEnum x | x < 0 = throw Underflow
| otherwise = S . toEnum $ pred x
fromEnum Z = 0
fromEnum (S x) = succ $ fromEnum x
enumFrom x = x : enumFrom (S x)
instance Num Nat where
Z + x = x
(S x) + y = S $ x + y
Z * _ = Z
(S x) * y = y + (x * y)
abs = id
signum Z = Z
signum _ = S Z
fromInteger 0 = Z
fromInteger x | x < 0 = throw Underflow
| otherwise = S . fromInteger $ pred x
x - Z = x
(S x) - (S y) = x - y
_ - _ = throw Underflow
negate Z = Z
negate _ = throw Underflow
instance Real Nat where
toRational = toRational . toInteger
instance Integral Nat where
quot x y = fromInteger $ quot (toInteger x) (toInteger y)
rem x y = fromInteger $ rem (toInteger x) (toInteger y)
div x y = fromInteger $ div (toInteger x) (toInteger y)
mod x y = fromInteger $ mod (toInteger x) (toInteger y)
quotRem x y = let (x, y) = quotRem (toInteger x) (toInteger y) in (fromInteger x, fromInteger y)
divMod x y = let (x, y) = divMod (toInteger x) (toInteger y) in (fromInteger x, fromInteger y)
toInteger Z = 0
toInteger (S x) = succ $ toInteger x
data Vec :: Nat -> * -> * where
Nil :: Vec Z a
Cons :: a -> Vec x a -> Vec (S x) a
data ReadableVec :: * -> * where
ReadableVec :: Vec x a -> ReadableVec a
instance Read a => Read (ReadableVec a) where
readsPrec x s = map (\(xs, r) -> (l2rv xs, r)) (readsPrec x s)
where
l2rv [] = ReadableVec Nil
l2rv (x : xs) = case l2rv xs of
ReadableVec rs -> ReadableVec (Cons x rs)
instance Show a => Show (Vec x a) where
showsPrec p xs = showsPrec p (ReadableVec xs)
instance Show a => Show (ReadableVec a) where
showsPrec p xs = showsPrec p (rv2l xs)
where
--rv2l :: ReadableVec x -> [x]
rv2l (ReadableVec Nil) = []
rv2l (ReadableVec (Cons x xs)) = x : rv2l (ReadableVec xs)GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Prelude> :load Vec.hs
[1 of 1] Compiling Main ( Vec.hs, interpreted )
Vec.hs:79:22: error:
• Could not deduce (Show a0) arising from a use of ‘showsPrec’
from the context: Show a
bound by the instance declaration at Vec.hs:78:10-39
The type variable ‘a0’ is ambiguous
These potential instances exist:
instance Show ArithException -- Defined in ‘GHC.Exception’
instance Show ErrorCall -- Defined in ‘GHC.Exception’
instance Show SomeException -- Defined in ‘GHC.Exception’
...plus 27 others
...plus 12 instances involving out-of-scope types
(use -fprint-potential-instances to see them all)
• In the expression: showsPrec p (rv2l xs)
In an equation for ‘showsPrec’:
showsPrec p xs
= showsPrec p (rv2l xs)
where
rv2l (ReadableVec Nil) = []
rv2l (ReadableVec (Cons x xs)) = x : rv2l (ReadableVec xs)
In the instance declaration for ‘Show (ReadableVec a)’
Vec.hs:82:34: error:
• Couldn't match expected type ‘t’ with actual type ‘[t0]’
‘t’ is untouchable
inside the constraints: x ~ 'Z
bound by a pattern with constructor: Nil :: forall a. Vec 'Z a,
in an equation for ‘rv2l’
at Vec.hs:82:27-29
‘t’ is a rigid type variable bound by
the inferred type of rv2l :: ReadableVec t1 -> t at Vec.hs:82:9
Possible fix: add a type signature for ‘rv2l’
• In the expression: []
In an equation for ‘rv2l’: rv2l (ReadableVec Nil) = []
In an equation for ‘showsPrec’:
showsPrec p xs
= showsPrec p (rv2l xs)
where
rv2l (ReadableVec Nil) = []
rv2l (ReadableVec (Cons x xs)) = x : rv2l (ReadableVec xs)
• Relevant bindings include
rv2l :: ReadableVec t1 -> t (bound at Vec.hs:82:9)
Vec.hs:83:46: error:
• Couldn't match type ‘t’ with ‘[t1]’
‘t’ is untouchable
inside the constraints: x ~ 'S x1
bound by a pattern with constructor:
Cons :: forall a (x :: Nat). a -> Vec x a -> Vec ('S x) a,
in an equation for ‘rv2l’
at Vec.hs:83:28-36
‘t’ is a rigid type variable bound by
the inferred type of rv2l :: ReadableVec t1 -> t at Vec.hs:82:9
Possible fix: add a type signature for ‘rv2l’
Expected type: ReadableVec t1 -> [t1]
Actual type: ReadableVec t1 -> t
• In the second argument of ‘(:)’, namely ‘rv2l (ReadableVec xs)’
In the expression: x : rv2l (ReadableVec xs)
In an equation for ‘rv2l’:
rv2l (ReadableVec (Cons x xs)) = x : rv2l (ReadableVec xs)
• Relevant bindings include
xs :: Vec x1 t1 (bound at Vec.hs:83:35)
x :: t1 (bound at Vec.hs:83:33)
rv2l :: ReadableVec t1 -> t (bound at Vec.hs:82:9)
Failed, modules loaded: none.Trac metadata
| Trac field | Value |
|---|---|
| Version | 8.0.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture |