[Haskell-cafe] What is GHC 7.8.2 doing here (typed holes, data+poly kinds, type families etc.)

[Dominic Mulligan]

Hi Erik,

Ahh, of course.  Thanks for that!

Dominic


On 16 June 2014 15:26, Erik Hesselink <hesselink at gmail.com> wrote:

> This seems right. The first argument you give to `substR` has type (m'
> + n) ~ (n + m'), so the rest is (f (m' + n) -> f (n + m')). The result
> type you have to provide is (S (m' + n) ~ n + S m'), so `f` is (S (m'
> + n) ~), which means your last argument should have type S (m' + n) ~
> m' + n, which is what ghci gives as the type of the hole.
>
> Erik
>
> On Mon, Jun 16, 2014 at 3:54 PM, Dominic Mulligan
> <dominic.p.mulligan at googlemail.com> wrote:
> > 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') _
> >
> > _______________________________________________
> > Haskell-Cafe mailing list
> > Haskell-Cafe at haskell.org
> > http://www.haskell.org/mailman/listinfo/haskell-cafe
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140616/f8821f74/attachment.html>