Why do these generic family instances conflict?

I am using GHC-8.0.1. This code (requires singletons lib):

{-# LANGUAGE TypeFamilies            #-}       
{-# LANGUAGE DataKinds               #-}
{-# LANGUAGE KindSignatures          #-}
{-# LANGUAGE TypeOperators           #-}
{-# LANGUAGE FlexibleInstances       #-}
{-# LANGUAGE FlexibleContexts        #-}           
{-# LANGUAGE ScopedTypeVariables     #-}
{-# LANGUAGE TypeInType              #-}
{-# LANGUAGE AllowAmbiguousTypes     #-}
{-# LANGUAGE GADTs                   #-}
{-# LANGUAGE ConstraintKinds         #-}

module Bug where

import Data.Kind
import Data.Singletons

type family MkCtx (kx :: Type) (kc :: Type) (c :: kc) (x :: kx) :: Constraint
type instance MkCtx kx (kx ~> Constraint) c x = Apply c x
type instance MkCtx kx (kx -> Constraint) c x = c x

      

with the message:

Conflicting family instance declarations:
      forall kx (x :: kx) (c :: kx ~> Constraint).
        MkCtx kx (kx ~> Constraint) c x = Apply c x
      forall kx (x :: kx) (c :: kx -> Constraint).
        MkCtx kx (kx -> Constraint) c x = c x

      

Why does the GHC consider these instances to be controversial? I can't see how they overlap.

UPDATE: GHC Confirmed Bug https://ghc.haskell.org/trac/ghc/ticket/13931

+3


source to share





All Articles