--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, NoMonomorphismRestriction #-}
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 xs (y : ys) where
usuccs xs = USucc (usuccs xs)
u x = usuccs (UOne x)
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> :set -XDataKinds
*Data.U> (u 'c')::U [String, Char, Int]
<interactive>:3:2: error:
• Overlapping instances for Usuccs (Char : xs0) '[Char, Int]
arising from a use of ‘u’
Matching instances:
instance [safe] Usuccs a a -- Defined at U.hs:25:10
...plus one instance involving out-of-scope types
(use -fprint-potential-instances to see them all)
(The choice depends on the instantiation of ‘xs0’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the expression: (u 'c') :: U '[String, Char, Int]
In an equation for ‘it’: it = (u 'c') :: U '[String, Char, Int]
--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 #-}
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 xs (y : ys) where
usuccs xs = USucc (usuccs xs)
u x = usuccs (UOne x)
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> :set -XDataKinds
*Data.U> (u 'c')::U [String, Char, Int]
<interactive>:3:2: error:
• No instance for (Usuccs (Char : xs0) '[])
arising from a use of ‘u’
• In the expression: (u 'c') :: U '[String, Char, Int]
In an equation for ‘it’: it = (u 'c') :: U '[String, Char, Int]
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 |
|