[Haskell-cafe] What is GHC 7.8.2 doing here (typed holes, data+poly kinds, type families etc.)
Dominic Mulligan
dominic.p.mulligan at googlemail.com
Mon Jun 16 13:54:58 UTC 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') _
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140616/bfbb6cd0/attachment.html>
More information about the Haskell-Cafe
mailing list