[GHC] #13950: IncoherentInstances

9 Jul 2017

      #13950: IncoherentInstances
-------------------------------------+-------------------------------------
           Reporter:  zaoqi          |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.2
           Keywords:                 |  Operating System:  Unknown/Multiple
  IncoherentInstances                |
       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, 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]
 }}}

 {{{#!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, 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]
 }}}

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13950
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler