Skip to content

Can't infer type

This is from an old ghc though (ghc 8.10.0.20191123):

{-# Language BlockArguments           #-}
{-# Language DerivingStrategies       #-}
{-# Language GADTs                    #-}
{-# Language InstanceSigs             #-}
{-# Language StandaloneKindSignatures #-}
{-# Language TypeApplications         #-}

import Type.Reflection
import Data.Kind
import Data.Maybe
import Control.Monad

type Name :: Type -> Type
data Name a
  = FreeName  String Int
  | BoundName Int Int
  deriving stock Eq

type AnyName :: Type
data AnyName where
  AnyName :: TypeRep a -> Name a -> AnyName

instance Eq AnyName where
  (==) :: AnyName -> AnyName -> Bool
  AnyName rep name == AnyName rep' name' = isJust @() do
    HRefl <- eqTypeRep rep rep'
    guard (name == name')

I tried this and it worked, but when I omitted the type argument for isJust

{-
error:
    • Couldn't match type ‘a0’ with ‘()’
        ‘a0’ is untouchable
          inside the constraints: (* ~ *, a1 ~ a)
          bound by a pattern with constructor:
                     HRefl :: forall k1 (a :: k1). a :~~: a,
                   in a pattern binding in
                        a 'do' block
          at ..:26:5-9
      Expected type: Maybe a0
        Actual type: Maybe ()
    • In a stmt of a 'do' block: guard (name == name')
      In the first argument of ‘isJust’, namely
        ‘do HRefl <- eqTypeRep rep rep'
            guard (name == name')’
      In the expression:
        isJust
          do HRefl <- eqTypeRep rep rep'
             guard (name == name')
   |
27 |     guard (name == name')
   |     ^^^^^^^^^^^^^^^^^^^^^
-}
instance Eq AnyName where
  (==) :: AnyName -> AnyName -> Bool
  AnyName rep name == AnyName rep' name' = isJust do
    HRefl <- eqTypeRep rep rep'
    guard (name == name')

but shouldn't it be able to infer the unit type?

Edited by Icelandjack
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information