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

[Erik Hesselink]

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
>