--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, TypeOperators, KindSignatures, GADTs,
MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, AllowAmbiguousTypes,
UndecidableInstances, IncoherentInstances, NoMonomorphismRestriction,
ScopedTypeVariables #-}
module Data.U where
data U :: [*] -> * where
UOne :: x -> U (x : xs)
USucc :: U xs -> U (x : xs)
class Usuccs a b where
usuccs :: U a -> U b
instance Usuccs a a where
usuccs = id
instance Usuccs xs ys => Usuccs (x : xs) (x : ys) where
usuccs (UOne x) = UOne x
usuccs (USucc xs) = USucc (usuccs xs)
instance Usuccs xs (x : xs) where
usuccs = USucc
instance Usuccs xs ys => Usuccs xs (y : ys) where
usuccs x = USucc (usuccs x)
u :: forall x xs. Usuccs '[x] xs => x -> U xs
u x = usuccs (UOne x :: U '[x])
class T a b where
t :: U a -> U b
instance Usuccs '[x] t => T '[x] t where
t (UOne x) = u x
instance (T xs t, Usuccs '[x] t) => T (x ': xs) t where
t (UOne x) = u x
t (USucc xs) = t xs
instance Eq x => Eq (U '[x]) where
UOne x == UOne y = x == y
instance (Eq x, Eq (U xs)) => Eq (U (x : xs)) where
UOne x == UOne y = x == y
USucc xs == USucc ys = xs == ys
_ == _ = False
instance Show x => Show (U '[x]) where
show (UOne x) = "(u " ++ showsPrec 11 x ")"
instance (Show x, Show (U xs)) => Show (U (x : xs)) where
show (UOne x) = "(u " ++ showsPrec 11 x ")"
show (USucc xs) = show xs
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Prelude> :load U.hs
[1 of 1] Compiling Data.U ( U.hs, interpreted )
Ok, modules loaded: Data.U.
*Data.U> :t u
u :: Usuccs '[x] xs => x -> U xs
--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, TypeOperators, KindSignatures, GADTs,
MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, AllowAmbiguousTypes,
UndecidableInstances, IncoherentInstances, NoMonomorphismRestriction,
ScopedTypeVariables #-}
module Data.U where
data U :: [*] -> * where
UOne :: x -> U (x : xs)
USucc :: U xs -> U (x : xs)
class Usuccs a b where
usuccs :: U a -> U b
instance Usuccs a a where
usuccs = id
instance Usuccs xs ys => Usuccs (x : xs) (x : ys) where
usuccs (UOne x) = UOne x
usuccs (USucc xs) = USucc (usuccs xs)
instance Usuccs xs (x : xs) where
usuccs = USucc
instance Usuccs xs ys => Usuccs xs (y : ys) where
usuccs x = USucc (usuccs x)
u :: Usuccs '[x] xs => x -> U xs
u x = usuccs (UOne x :: U '[x])
class T a b where
t :: U a -> U b
instance Usuccs '[x] t => T '[x] t where
t (UOne x) = u x
instance (T xs t, Usuccs '[x] t) => T (x ': xs) t where
t (UOne x) = u x
t (USucc xs) = t xs
instance Eq x => Eq (U '[x]) where
UOne x == UOne y = x == y
instance (Eq x, Eq (U xs)) => Eq (U (x : xs)) where
UOne x == UOne y = x == y
USucc xs == USucc ys = xs == ys
_ == _ = False
instance Show x => Show (U '[x]) where
show (UOne x) = "(u " ++ showsPrec 11 x ")"
instance (Show x, Show (U xs)) => Show (U (x : xs)) where
show (UOne x) = "(u " ++ showsPrec 11 x ")"
show (USucc xs) = show xs
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Prelude> :load U.hs
[1 of 1] Compiling Data.U ( U.hs, interpreted )
U.hs:39:7: error:
• Could not deduce (Usuccs '[x0] xs) arising from a use of ‘usuccs’
from the context: Usuccs '[x] xs
bound by the type signature for:
u :: Usuccs '[x] xs => x -> U xs
at U.hs:38:1-32
The type variable ‘x0’ is ambiguous
Relevant bindings include u :: x -> U xs (bound at U.hs:39:1)
• In the expression: usuccs (UOne x :: U '[x])
In an equation for ‘u’: u x = usuccs (UOne x :: U '[x])
U.hs:39:15: error:
• Couldn't match type ‘x’ with ‘x1’
‘x’ is a rigid type variable bound by
the type signature for:
u :: forall x (xs :: [*]). Usuccs '[x] xs => x -> U xs
at U.hs:38:6
‘x1’ is a rigid type variable bound by
an expression type signature:
forall x1. U '[x1]
at U.hs:39:25
Expected type: U '[x1]
Actual type: U '[x]
• In the first argument of ‘usuccs’, namely ‘(UOne x :: U '[x])’
In the expression: usuccs (UOne x :: U '[x])
In an equation for ‘u’: u x = usuccs (UOne x :: U '[x])
• Relevant bindings include
x :: x (bound at U.hs:39:3)
u :: x -> U xs (bound at U.hs:39:1)
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 |
|