Re: [GHC] #13950: IncoherentInstances

10 Jul 2017


      #13950: IncoherentInstances
-------------------------------------+-------------------------------------
        Reporter:  zaoqi             |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.2
      Resolution:                    |             Keywords:
                                     |  IncoherentInstances
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by hsyl20):

 {{{#!hs
 {-# LANGUAGE DataKinds, TypeOperators, KindSignatures, GADTs,
 MultiParamTypeClasses, FlexibleInstances, FlexibleContexts,
 AllowAmbiguousTypes,
 UndecidableInstances, IncoherentInstances, NoMonomorphismRestriction #-}

 {-# LANGUAGE 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)


 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

 u :: forall t x. Usuccs '[x] t => x -> U t
 u x = usuccs (UOne x :: U '[x])
 }}}

 {{{#!bash
...
:set -XDataKinds
(u 'c')::U [String, Char, Int]
 (u 'c')
 }}}
?

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