#14065: Type inference -------------------------------------+------------------------------------- Reporter: zaoqi | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs --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. }}} {{{#!hs --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. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14065 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler