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'
| ^
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.
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
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
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.