What is GHC 7.8.2 doing here (typed holes, data+poly kinds, type families etc.)

16 Jun 2014

      Hi,

I've come across some behaviour in GHC 7.8.2 which seems strange, and may
be a bug, but I wish to check before reporting it.  Consider the minimum
example pasted at the bottom of this message.  At the line

  plusComm (SS m') n' = _

GHC tells me that I have a single hole in the file with type

  'S (m1 :+: n) :~: (n :+: 'S m1)

which is straightforward to provide, by rewriting with the inductive
hypothesis (a recursive call of plusComm) and then some fiddling.  However,
replacing this line with the refinement

  plusComm (SS m') n' = substR (plusComm m' n') _

GHC tells me that the remaining hole now has type

  'S (m1 :+: n) :~: (m1 :+: n)

which seems completely incorrect to me.  Shouldn't this hole have type

  'S (n :+: m1) :~: (n :+: S m1)

?  Can anybody give any clues as to what is happening?

Thanks,
Dominic

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module MinimumExample where

  data (:~:) (a :: k) (b :: k) where
    Refl :: a :~: a

  substR :: a :~: b -> f a -> f b
  substR Refl x = x

  substL :: a :~: b -> f b -> f a
  substL Refl x = x

  cong :: a :~: b -> f a :~: f b
  cong Refl = Refl

  data Nat where
    Z :: Nat
    S :: Nat -> Nat

  data NatS (m :: Nat) where
    ZS :: NatS Z
    SS :: NatS m -> NatS (S m)

  type family (:+:) (m :: Nat) (n :: Nat) :: Nat where
    Z   :+: n = n
    (S m) :+: n = S (m :+: n)

  plusZRightNeutral :: NatS m -> (m :+: Z) :~: m
  plusZRightNeutral ZS      = Refl
  plusZRightNeutral (SS m') = cong (plusZRightNeutral m')

  plusComm :: NatS m -> NatS n -> (m :+: n) :~: (n :+: m)
  plusComm ZS      n' = substL (plusZRightNeutral n') Refl
  -- everything seems correct here
  plusComm (SS m') n = _
  -- but things look completely incorrect, here
  -- plusComm (SS m') n' = substR (plusComm m' n') _

Dominic Mulligan

Erik Hesselink

Dominic Mulligan

tags

participants (2)