Understanding type inference in pattern matching

Learn
#1

I’m investigating the following type inference issue where isIdX1 type checks, but isIdX2 does not:

#! /usr/bin/env nix-shell
#! nix-shell -p "haskell.packages.ghc902.ghcWithPackages (pkgs: with pkgs; [ base ])"
#! nix-shell --pure
#! nix-shell -i runghc
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}

module Main where

infixr 5 ~>

data Term t where
  Apply :: (x ~> t) -> x -> Term t

data Simple where
  X :: Simple
  Simple :: Term Simple -> Simple

isIdX1 :: Simple -> Bool
isIdX1 simple = case simple of
  Simple fx -> case fx of
     Apply f x -> True          -- Type checks correctly
  _ -> False

isIdX2 :: Simple -> Bool
isIdX2 simple = case simple of
  Simple (Apply f X) -> True    -- Couldn't match expected type `x' with actual type `Simple'
  _ -> False

data (a ~> b) where
  Id :: Simple ~> Simple

Is there a workaround I can use to avoid breaking down the case analysis into multiple case statements without breaking type inference? I’m grateful for any guidance.

The full type error looks like this:

Main.hs:28:19: error:
    * Couldn't match expected type `x' with actual type `Simple'
      `x' is a rigid type variable bound by
        a pattern with constructor:
          Apply :: forall x t. (x ~> t) -> x -> Term t,
        in a case alternative
        at Main.hs:28:11-19
    * In the pattern: X
      In the pattern: Apply f X
      In the pattern: Simple (Apply f X)
    * Relevant bindings include
        f :: x ~> Simple (bound at Main.hs:28:17)
   |
28 |   Simple (Apply f X) -> True    -- Couldn't match expected type `x' with actual type `Simple'
   |                   ^
#2

I think the confusion is just because the two functions are not the same at all. The function isIdX1 has a lowercase x in the pattern and isIdX2 has an uppercase X. If you make both lowercase they both type check and if you make both uppercase they both fail to type check.

1 Like
#3

handpalm. Ugh, sorry about that.

Slightly modified question, if anyone is willing to follow up:

isIdX3 :: Term Simple -> Bool
isIdX3 fx = case fx of
  Apply f X -> True  -- Couldn't match expected type `x' with actual type `Simple'
  _ -> False

isIdX4 :: Term Simple -> Bool
isIdX4 fx = case fx of
  Apply Id X -> True  -- typechecks
  _ -> False

This is what I was originally trying to grok.

(EDIT: simplified)

#4

Observe that if you change the order of the parameters of Apply it does not work, so I guess you’ve hit a corner case in the type checker where the order of type checking matters. My guess is that in isIdX4, Id is checked first, which allows x ~ t to be deduced. t ~ Simple is already known. So x ~ Simple is deduced and X type checks. Without that, the argument X cannot be type checked.

infixr 5 ~>

data Term t where
  Apply :: x -> (x ~> t) -> Term t

data Simple where
  X :: Simple
  Simple :: Term Simple -> Simple

data (a ~> b) where
  Id :: Simple ~> Simple

isIdX5 :: Term Simple -> Bool
isIdX5 fx = case fx of
  Apply X Id -> True  -- still doesn't work
  _ -> False
1 Like
#5

With fresh eyes and an afternoon away, my foolish error is now obvious to me since it boils down to the same sort of thing as

data Foo r where
  Foo :: x -> Foo r

unFoo :: Foo () -> a
unFoo (Foo x) = x  -- type of x obviously can't escape out of Foo

Live and learn :man_shrugging:

#6

I’m not sure it’s quite the same. In unFoo the type of x really is escaping outside the (desugared) case expression. In isIdX5 it doesn’t appear anywhere outside the case expression, it just doesn’t unify earlier enough with what you’d want it to.

#7

Ah yep I agree it’s isn’t the same issue as in isIdX5 where there really is an issue with the order of type checking.

However my original lapse in understanding was wrt the pattern Apply _ X causing issues with type inference whereas the pattern Apply Id X does not.

I think that the pattern Apply _ X resembles Foo X, and this does not type check either:

unFoo2 :: Foo () -> Bool
unFoo2 foo = case foo of 
  Foo "A" -> True -- Couldn't match expected type `x' with actual type `String'
  _ -> False
1 Like