I’m investigating the following type inference issue where isIdX1
type checks, but isIdX2
does not:
#! /usr/bin/env nixshell
#! nixshell p "haskell.packages.ghc902.ghcWithPackages (pkgs: with pkgs; [ base ])"
#! nixshell pure
#! nixshell 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:1119
* 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'
 ^