Opened 4 years ago

Closed 4 years ago

Last modified 4 years ago

#10805 closed bug (fixed)

Could not deduce (a ~ b) implies (f a ~ f b), because a type function may not be injective

Reported by: htebalaka Owned by:
Priority: normal Milestone: 8.0.1
Component: Compiler (Type checker) Version: 7.10.2
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

I don't know if the summary I provided is what's really going on here, but I'm a little baffled why this doesn't typecheck. I can't see what injectivity has to do with it, since we're not trying to deduce that the arguments are the same from the result of an application being the same; rather we're doing the opposite. I've encountered plenty of obvious arithmetic laws that I've needed to unsafeCoerceConstraint away with doing type level arithmetic, but this seems like it should be trivial regardless.

{-# LANGUAGE GADTs, ExplicitNamespaces, TypeOperators, DataKinds #-}
{-# LANGUAGE ConstraintKinds, KindSignatures, PatternGuards #-}

import Data.Type.Equality ((:~:)(..))
import GHC.TypeLits (Nat, type (<=), type (-), type (+), type (<=?))

data SNat :: Nat -> * where
    SSucc   :: SNat a -> SNat (a + 1)
    SZero   :: SNat 0

heqHet :: SNat a -> SNat b -> Maybe (a :~: b)
heqHet SZero SZero = Just Refl
heqHet (SSucc a) (SSucc b)
    | Just Refl <- heqHet a b = Just Refl
heqHet _ _ = Nothing

data Slice :: Nat -> Nat -> * where
    Slice   :: ((start + 1) <= end, end <= numElements)
            => SNat numElements -> SNat start -> SNat end
            -> Slice numElements (end - start)

heqHet' :: Slice a b -> Slice a b' -> Bool
heqHet' (Slice _ start end) (Slice _ start' end')
    | Just _ <- heqHet start start'
    , Just _ <- heqHet end end' = True
    | otherwise = False
Slice.hs:24:10:
    Could not deduce (((start + 1) <=? a) ~ ((start + 1) <=? a))
    from the context (b ~ (end - start), (start + 1) <= end, end <= a)
      bound by a pattern with constructor
                 Slice :: forall (numElements :: Nat) (start :: Nat) (end :: Nat).
                          ((start + 1) <= end, end <= numElements) =>
                          SNat numElements
                          -> SNat start -> SNat end -> Slice numElements (end - start),
               in an equation for heqHet'
      at Slice.hs:24:10-26
    or from (b' ~ (end1 - start1), (start1 + 1) <= end1, end1 <= a)
      bound by a pattern with constructor
                 Slice :: forall (numElements :: Nat) (start :: Nat) (end :: Nat).
                          ((start + 1) <= end, end <= numElements) =>
                          SNat numElements
                          -> SNat start -> SNat end -> Slice numElements (end - start),
               in an equation for heqHet'
      at Slice.hs:24:30-48
    NB: GHC.TypeLits.<=? is a type function, and may not be injective
    Relevant bindings include
      heqHet' :: Slice a b -> Slice a b' -> Bool (bound at Slice.hs:24:1)
    In the pattern: Slice _ start end
    In an equation for heqHet':
        heqHet' (Slice _ start end) (Slice _ start' end')
          | Just _ <- heqHet start start', Just _ <- heqHet end end' = True
          | otherwise = False
Failed, modules loaded: none.

Change History (3)

comment:1 Changed 4 years ago by htebalaka

Resolution: fixed
Status: newclosed

I found https://ghc.haskell.org/trac/ghc/ticket/10742, which appears to be the same thing and is fixed in HEAD, so I'm closing

comment:2 Changed 4 years ago by simonpj

Yes, it works fine in HEAD... I checked.

comment:3 Changed 4 years ago by thomie

Milestone: 8.0.1
Note: See TracTickets for help on using tickets.