Why these type family instances conflicting?

Viewed 115

I'm using GHC-8.0.1. This code (requires the 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 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 GHC considers these instances conflicting? I don't see how they overlap.

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

0 Answers
Related