[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 14:32:52 UTC 2014
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>
More information about the Haskell-Cafe
mailing list