IncoherentInstances

--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