[GHC] #14065: Type inference

31 Jul 2017


      #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